Not checking for closure under stuttering | Zendy

Gerard J. Holzmann | Zendy; Orna Kupferman | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Not checking for closure under stuttering

Author(s) -

Gerard J. Holzmann,

Orna Kupferman

Publication year - 1997

Publication title -

dimacs series in discrete mathematics and theoretical computer science

Language(s) - English

Resource type - Book series

eISSN - 2472-4793

pISSN - 1052-1798

DOI - 10.1090/dimacs/032/02

Subject(s) - stuttering , correctness , closure (psychology) , order (exchange) , pity , spin (aerodynamics) , extension (predicate logic) , computer science , mathematics , programming language , psychology , audiology , medicine , engineering , social psychology , economics , market economy , finance , aerospace engineering

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 counter-example that SPIN provides to determine whether the program is correct with respect to N or that N is not closed under stuttering.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research