A Formal Model of a Multi-step Coordination Protocol for Self-adaptive Software Using Coloured Petri Nets

International audienceTechnology advances continue to make computing environments ever changing and more complex. In the presence of such environments software systems are increasingly expected to continue operating at run-time. As human intervention becomes costly, time-consuming and error-prone, these systems should be equipped with self-adaptation capabilities in order to adapt themselves in response to environmental changes. While most of the research in this area focuses on individual parts of an adaptive system, our work leverages on this research but tackles the problem where interdependent and distributed adaptations are concurrently performed. In this paper, we approach behavioural changes of component-based systems in two stages. First, we propose a process to individually adapt one component at a time. Second, we elaborate a coordination protocol to maintain globally consistent state when implementing distributed adaptations. To achieve correct coordination, rather than only considering dependency relations between multiple adaptations, our approach further focuses on dependency relations between components at run-time. Motivated by the potential benefits of using formalisms, we construct a formal model of our protocol using Coloured Petri Nets in order for an adaptive system to be trusted after adaptation. In the model, we make sufficient abstraction of details, but still deal with the core of the protocol. This makes the model simpler and the analysis easier due to restricted state space size. We verify key behavioural properties and conduct CTL model checking to assess the correctness of the model and thereby the correctness of the protocol