2009 | OriginalPaper | Chapter
Assume-Guarantee Verification of Concurrent Systems
Authors : Liliana D’Errico, Michele Loreti
Published in: Coordination Models and Languages
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Process algebras are a set of mathematically rigourous languages with well defined semantics that permit modelling behaviour of concurrent and communicating systems. Verification of concurrent systems within the process algebraic approach can be performed by checking that processes enjoy properties described by some temporal logic’s formulae. In this paper we present a formal framework that permits verifying properties of concurrent and communicating systems by using an assumption-guarantee approach. Each system component is not considered in isolation, but in conjunction with assumptions about the context of the component. In the paper we introduce a sound and complete proof system that permits verifying whether a process, when it is executed in an environment for which we provide some assumptions, satisfies a given formula. It is also ensured that property satisfaction is preserved whenever the context is partially instantiated (implemented) as a concrete process that verifies the assumptions we have for the environment.