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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-00909368
Contributor : Davide Sangiogi <>
Submitted on : Tuesday, November 26, 2013 - 11:07:30 AM
Last modification on : Wednesday, January 23, 2019 - 2:38:28 PM

Identifiers

Collections

INRIA | CEA | DRT | LIST

Citation

Mario Bravetti, Cinzia Di Giusto, Jorge A. Pérez, Gianluigi Zavattaro. Towards the Verification of Adaptable Processes. 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. pp.269--283, ⟨10.1007/978-3-642-34026-0_20⟩. ⟨hal-00909368⟩

Share

Metrics

Record views

354