[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Eurosys 2023 paper: Model Checking Guided Testing for Distributed Systems



Eurosys 2023 paper  and  the  Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 both focus to verify the impl code. and the aws lightweigh method is to seperate the whole  to mulitple properties to verfify.
And the   How Amazon Web Services Uses Formal Methods just focus high specs ,not the impl code. 


在2023年5月26日星期五 UTC+8 00:19:57<Alex Weisberger> 写道:
I read closer, and the MongoDB paper (eXtreme Modelling in Practice) is cited here too.

On Thu, May 25, 2023 at 12:14 PM Alex Weisberger <alex.m.w...@xxxxxxxxx> wrote:
This is awesome, thanks for sharing.

This sounds very similar to the model-based test case generation approach taken in this MongoDB paper: https://dl.acm.org/doi/abs/10.14778/3397230.3397233. The main difference here is that Mocket uses annotations in the implementation code to provide a mapping for state variables / actions. I think this is a really good idea, because it removes the need to introduce yet another tool into the workflow. I wonder what limitations exist on the annotations in practice, but it definitely seems like an interesting direction overall.

Re the citations, the paper does cite "How Amazon Web Services Uses Formal Methods," so the authors definitely are aware of Amazon's usage of TLA+. "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" uses property-based testing to generate test cases for the implementation, so it's not exactly an apples-to-apples comparison. I didn't find that this omission took anything away from the paper.



On Thu, May 25, 2023 at 1:12 AM chunxiao B <ine...@xxxxxxxxx> wrote:
The paper did  not cite the “Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3” so  ...

在2023年5月25日星期四 UTC 03:20:58<Aman Shaikh> 写道:

The paper can be found at: https://dl.acm.org/doi/10.1145/3552326.3587442

Code for the tool described in the paper at: https://github.com/tcse-iscas/Mocket.

aman


--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ad364d5b-39aa-4ce2-bda7-0b5e484c0cb7n%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e9c37380-8b3c-4550-a684-4ec5a6eb65b5n%40googlegroups.com.