Formal Verification of Self-Adaptive Behaviors in Decentralized Systems with Uppaal : An Initial Study
M. Usman Iftikhar, Danny Weyns · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2012
Ensuring the required qualities of software systems that have to operate in highly dynamic environments poses a tremendous engineering challenge.Self-adaptive software is generally considered as one of the most promising approaches to manage the complexity of modern software systems. Our particularinterest is in decentralized self-adaptive systems, in which central control of adaptation is not an option. One major challenge in self-adaptive systems, in particularthose with decentralized control of adaptation, is to provide guarantees about theintended runtime quality properties. This paper reports a first step of our researchon a formally founded approach to validate behavioral properties of decentralizedself-adaptive systems to guarantee the required systems qualities. We contributewith a formal model of a decentralized traffic monitoring system and prove anumber of self-adaptation properties for flexibility and robustness. To model themain processes in the system, we use timed automata, and for the specificationof the required properties, we use timed computation tree logic. For the actualmodeling, we use the Uppaal tool that provides an integrated environment formodeling, simulation and verification of the system.