Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol
Keyword(s):
We present a case study of the verification of parameterized mutual exclusion protocol using finite model finder Mace4. Thhe verification follows an approach based on modeling of reachability between states of the protocol as deducibility between appropriate encodings of states by first-order predicate logic formulae. The result of successful verification is a finite countermodel, a witness of non-deducibility, which represents a system invariant.
1999 ◽
Vol 9
(4)
◽
pp. 335-359
◽
Keyword(s):
1992 ◽
Vol 71
(3_suppl)
◽
pp. 1091-1104
◽
Keyword(s):
Keyword(s):