Universal properties verification of parameterized parallel systems

Abstract

This paper presents a method for verifying universal properties of parameterized parallel systems using Parameterized Predicate Diagrams [10]. Parameterized Predicate Diagrams are diagrams which are used to represent the abstractions of such systems described by specifications written in temporal logic. This method presented here integrates deductive verification and algorithmic techniques. Non-temporal proof obligations establish the correspondence between the original specification and the diagram, whereas model checking can be used to verify properties over finite-state abstractions. © Springer-Verlag Berlin Heidelberg 2005.