[tlaplus] More Sophisticated Forms of Model Checking

["hengx...@xxxxxxxxx" <hengxin0912@xxxxxxxxx>]

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?

Thanks.

Best regards,

Hengfeng Wei

-- 
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.