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.
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: 08 Feb 2018 *