Not checking for closure under stuttering. (English) Zbl 0889.68102
Grégoire, Jean-Charles (ed.) et al., The SPIN verification system. The 2nd workshop, proceedings of a DIMACS workshop. Rutgers Univ., New Brunswick, NJ, USA; August 5, 1996. Providence, RI: AMS, American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 32, 17-22 (1997).
Summary: The model checker SPIN works better with specifications that are closed under stuttering. Checking such specifications, SPIN can use its partial-order reductions. It is hard to check whether a given specification is closed under stuttering and it is pity to give up SPIN’s partial-order reductions. We suggest an algorithm that, given a program \(P\) and a specification \(N\) of bad behaviors for \(P\), checks the correctness of \(P\) with respect to an extension \(N'\) of \(N\) that is guaranteed to be closed under stuttering. In this check, SPIN can use its partial-order reductions. If \(P\) is correct with respect to \(N\), we conclude that it is correct also with respect to \(N\). If \(P\) is not correct with respect to \(N'\), we use the counterexample that SPIN provides to determine whether the program is correct with respect to \(N\) or that \(N\) is not closed under stuttering.
For the entire collection see [Zbl 0868.00062].
For the entire collection see [Zbl 0868.00062].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
