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.

Assume-Guarantee Verification of Concurrent Systems

Michele Loreti
2009-01-01

Abstract

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11581/405010
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact