Coordination models and languages are introduced to effectively rule and govern the interactions in those systems that feature complexity, distribution, opennes and high dynamics. These characteristics, however, traditionally impose a number of constraints on the engineering process: most notably, they make system specifications infinite, thus complicating - and sometimes preventing - the successful automatic verification of properties. In the field of verification for infinite state systems, the notion of well-structured transition systems has recently being introduced and studied. Its framework not only unifies a number of existing results in the context of infinite verification, but also introduces general concepts and methodologies, such as upward-closure and backward analysis, that show a great potential applicability for concurrent and interactive systems in general. In this paper, we evaluate the applicability of this framework to the context of coordination, formally defining the notion of well-structured coordination. A coordinated system adhering to this notion is amenable to a description in terms of a well-structured transition system, where interesting properties concerning termination, boundedness, safety, and liveness are decidable. An example of application to the Linda coordination model is studied, focussing on a methodology for proving the safety properties of coordinated systems.

Mirko Viroli (2004). Verifying Properties of Coordination by Well-Structured Transition Systems. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 97, 67-96 [10.1016/j.entcs.2004.04.032].

Verifying Properties of Coordination by Well-Structured Transition Systems

VIROLI, MIRKO
2004

Abstract

Coordination models and languages are introduced to effectively rule and govern the interactions in those systems that feature complexity, distribution, opennes and high dynamics. These characteristics, however, traditionally impose a number of constraints on the engineering process: most notably, they make system specifications infinite, thus complicating - and sometimes preventing - the successful automatic verification of properties. In the field of verification for infinite state systems, the notion of well-structured transition systems has recently being introduced and studied. Its framework not only unifies a number of existing results in the context of infinite verification, but also introduces general concepts and methodologies, such as upward-closure and backward analysis, that show a great potential applicability for concurrent and interactive systems in general. In this paper, we evaluate the applicability of this framework to the context of coordination, formally defining the notion of well-structured coordination. A coordinated system adhering to this notion is amenable to a description in terms of a well-structured transition system, where interesting properties concerning termination, boundedness, safety, and liveness are decidable. An example of application to the Linda coordination model is studied, focussing on a methodology for proving the safety properties of coordinated systems.
2004
Mirko Viroli (2004). Verifying Properties of Coordination by Well-Structured Transition Systems. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 97, 67-96 [10.1016/j.entcs.2004.04.032].
Mirko Viroli
File in questo prodotto:
Eventuali allegati, non sono esposti

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/11585/9596
 Attenzione

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

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