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