Towards the Verification of Adaptable Processes

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.
Type de document :
Communication dans un congrès
Tiziana Margaria and Bernhard Steffen. Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium (ISoLA 2012), Proceedings, Part I, 2012, Heraklion, Crète, Greece. Springer, 7609, pp.269--283, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-34026-0_20〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00909368
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 11:07:30
Dernière modification le : jeudi 11 janvier 2018 - 16:22:41

Identifiants

Collections

Citation

Mario Bravetti, Cinzia Di Giusto, Jorge A. Pérez, Gianluigi Zavattaro. Towards the Verification of Adaptable Processes. Tiziana Margaria and Bernhard Steffen. Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium (ISoLA 2012), Proceedings, Part I, 2012, Heraklion, Crète, Greece. Springer, 7609, pp.269--283, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-34026-0_20〉. 〈hal-00909368〉

Partager

Métriques

Consultations de la notice

252