Title: Modelling, specifying and verifying self-adaptive systems instantiating MAPE patterns

Authors: Marwa Hachicha; Riadh Ben Halima; Ahmed Hadj Kacem

Addresses: REDCAD Laboratory, University of Sfax, B.P. 1173, Sfax, Tunisia ' REDCAD Laboratory, University of Sfax, B.P. 1173, Sfax, Tunisia ' REDCAD Laboratory, University of Sfax, B.P. 1173, Sfax, Tunisia

Abstract: Self-adaptive systems are able to modify their behaviour and/or structure to deal with their continuously changing environment and internal dynamics. Adaptive systems are generally more difficult to design, specify and verify owing to their high complexity. Ensuring the correctness of the system adaptation logic is very crucial. This correctness also depends on the time associated with events. In this paper, we propose a refinement approach that aims first at modelling step-by-step self-adaptive systems that instantiate MAPE patterns for decentralised control in self-adaptive systems. Second, these models are then automatically translated into Event-B specifications that can be proved using the Rodin theorem prover. This formal specification provides a way to verify several relevant properties for self-adaptive systems. We distinguish between three classes of properties: adaptation, system and temporal properties. We illustrate our approach by modelling and verifying the forest fire detection system that exhibits a self-adaptive behaviour.

Keywords: self-adaptive systems; MAPE control loop; MAPE patterns; structural; behavioural; modelling; Event-B method; formal verification.

DOI: 10.1504/IJCAT.2018.090029

International Journal of Computer Applications in Technology, 2018 Vol.57 No.1, pp.28 - 44

Received: 02 Oct 2016
Accepted: 19 Jan 2017
Published online: 27 Feb 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article