[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] More Sophisticated Forms of Model Checking
- From: "hengx...@xxxxxxxxx" <hengxin0912@xxxxxxxxx>
- Date: Sat, 7 Aug 2021 00:32:01 -0700 (PDT)
- Ironport-hdrordr: A9a23:eL/1Y6F0gHkN6DgCpLqEPseALOsnbusQ8zAXPjNKJCC9Ffb2qynOppgmPHrP4wr5N0tQ4+xoR5PwJU80maQV3WBpB8bFYOCFghrQEGgS1+HfKlTbckXDH4hmtZuIGJIRNDSfNykYse/KpC6cM/tI+qjkzImYwdzV1mpMYGhRGtpdBy0TMHf/LqVTLzM2eKbQV/enl7J6TpGbCBMqUvg=
I am reading the paper "Real Time is Really Simple" by Leslie Lamport.
It reads at the beginning of Section 6.1:
"Model checking a specification consists of mechanically verifying that all
possible executions satisfy the desired correctness properties. Specifications
typically contain unspecified parameters, such as the number of processes
or the size of a buffer. Ordinary model checking is performed for specific
instances of the specification obtained by substituting actual values for the
parameters. The likelihood that model checking has missed an error in the
specification depends on the variety of different instances that have been
checked. There are more sophisticated forms of model checking that employ
abstraction techniques, sometimes with simple mechanical theorem check-
ing, to verify the specification for all values of the parameters."
Do you know any resources for such "more sophisticated forms of model checking", such as papers and examples?
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/bef985b2-f0df-4aba-b40f-a2922d828b50n%40googlegroups.com.