Towards the Verification of Adaptable Processes

M. Bravetti, C. Di Giusto, J.A. Pèrez and G. Zavattaro
In ISoLA 2012, volume 7609 of LNCS, pp 269-283, 2012.
In prior work, with the aim of formally modeling and analyzing the behavior of concurrent processes with forms of dynamic evolution, we have pro- posed 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.