Property-preserving refinement of concurrent systems

Abstract

Verification of concurrent systems within the process algebraic approach can be performed by checking that processes enjoy properties described by formulae of a temporal logic. However, to use these approach a complete description of the considered system has to be provided. In a previous work we propose a formal framework based on an assumption-guarantee approach where each system component is not considered in isolation, but in conjunction with assumptions about the context of the component. In the present paper we propose a procedure to refine the set of context assumptions. In each of the refinement steps the environment is partially instantiated with a process algebraic term while formulae satisfaction is preserved. © 2010 Springer-Verlag Berlin Heidelberg.