|
Abstract : |
The model checker Spin works better with speci cations that are closed under stuttering. Checking such speci cations, Spin can use its partial-order reductions. It is hard to check whether a given speci cation is closed under stuttering and it is pity to giveupSpin's partial-order reductions. We suggest an algorithm that, given a program P and a speci cation N of bad behaviors for P,checks the correctness of P with respect to an extension N 0 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 0,we conclude that it is correct also with respect to N. If P is not correct with respect to N 0,we use the counter-example that Spin provides to determine whether the program is correct with respect to N or that N is not closed under stuttering. 1, |
