The paper presents the method of network invariants for verifying a wide spectrum of LTL properties, including liveness, of parameterized systems. This method can be applied to establish the validity of the property over a system S(n) for every value of the parameter n. The application of the method requires checking abstraction relations between two finite-state systems. We present a proof rule, based on the method of Abstraction Mapping by Abadi and Lamport, which has been implemented on the TLV model checker and incorporates both history and prophecy variables. The effectiveness of the network invariant method is illustrated on several examples, including a deterministic and probabilistic versions of the dining-philosophers problem.
展开▼
