Main Article Content
Abstract
This paper presents the verification of mutual-exclusion properties of parameterized reader-writer algorithm. A class of diagram called Predicate diagrams [1] is used for representing the abstractions of parameterized systems described by specifications written in TLA. The verification is done by integrating deductive verification and algorithmic techniques. The correspondence between the original specification and the diagram is established by non-temporal proof obligations. Whereas model checker SPIN [3] is used to verify properties over finite-state abstractions.
Keywords: formal method, verification, parameterized system, temporal logic.
Keywords: formal method, verification, parameterized system, temporal logic.