In prior work, with the aim of formally modeling and analyzing the behavior of concurrent processes with forms of dynamic evolution, we have proposed a process calculus of adaptable processes. Our proposal addressed the (un)decidability of two safety properties related to error occurrence. In order to allow for a more comprehensive verification framework for adaptable processes, the ability to express general properties is most desirable. In this paper we address this important issue: we explain how the proof techniques for (un)decidability results for adaptable processes generalize to a simple yet expressive temporal logic over adaptable processes.We provide examples of the expressiveness of the logic and its significance in relation with the calculus of adaptable processes.

Mario Bravetti, Cinzia Giusto, Jorge A. Pérez, Gianluigi Zavattaro (2012). Towards the Verification of Adaptable Processes. Berlin : Springer [10.1007/978-3-642-34026-0_20].

Towards the Verification of Adaptable Processes

BRAVETTI, MARIO;ZAVATTARO, GIANLUIGI
2012

Abstract

In prior work, with the aim of formally modeling and analyzing the behavior of concurrent processes with forms of dynamic evolution, we have proposed a process calculus of adaptable processes. Our proposal addressed the (un)decidability of two safety properties related to error occurrence. In order to allow for a more comprehensive verification framework for adaptable processes, the ability to express general properties is most desirable. In this paper we address this important issue: we explain how the proof techniques for (un)decidability results for adaptable processes generalize to a simple yet expressive temporal logic over adaptable processes.We provide examples of the expressiveness of the logic and its significance in relation with the calculus of adaptable processes.
2012
Proceedings of Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium, ISoLA 2012, part I
269
283
Mario Bravetti, Cinzia Giusto, Jorge A. Pérez, Gianluigi Zavattaro (2012). Towards the Verification of Adaptable Processes. Berlin : Springer [10.1007/978-3-642-34026-0_20].
Mario Bravetti;Cinzia Giusto;Jorge A. Pérez;Gianluigi Zavattaro
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/145466
 Attenzione

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

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