Title: A Model-Based Approach to Engineer Self-Adaptive Systems with Guarantees
Subject: Computer and Information Sciences
Faculty: Faculty of Technology
Date: Monday 18 December 2017 at 1.15 pm
Location: Room C1202 (Newton), building C, Växjö
External reviewer: Professor Flavio Oquendo, Université Bretagne Sud, France
Examining committee: Associate Professor Patrizio Pelliccione, Gothenburg University, Sweden; Associate Professor Romina Spalazzese, Malmö University, Sweden; Professor Danny Hughes, KU Leuven, Belgium
Examiner: Professor Welf Löwe, Department of Computer Science, Linnaeus University
Supervisor: Professor Danny Weyns, Department of Computer Science, Linnaeus University
Chairman: Associate Professor Jonas Lundberg, Department of Computer Science, Linnaeus University
Spikning: Friday 1 December 2017 at 2.00 pm at the university library in Växjö
Modern software systems are increasingly characterized by uncertainties in the operating context and user requirements. These uncertainties are difficult to predict at design time. Achieving the quality goals of such systems depends on the ability of the software to deal with these uncertainties at runtime.
A self-adaptive system employs a feedback loop to continuously monitor and adapt itself to achieve particular quality goals (i.e., adaptation goals) regardless of uncertainties. Current research applies formal techniques to provide guarantees for adaptation goals, typically using exhaustive verification techniques. Although these techniques offer strong guarantees for the goals, they suffer from well-known state explosion problem.
In this thesis, we take a broader perspective and focus on two types of guarantees: (1) functional correctness of the feedback loop, and (2) guaranteeing the adaptation goals in an efficient manner. To that end, we present ActivFORMS (Active FORmal Models for Self-adaptation), a formally founded model-driven approach for engineering self-adaptive systems with guarantees.
ActivFORMS achieves functional correctness by direct execution of formally verified models of the feedback loop using a reusable virtual machine. To efficiently provide guarantees for the adaptation goals with a required level of confidence, ActivFORMS applies statistical model checking at runtime.
ActivFORMS supports on the fly changes of adaptation goals and updates of the verified feedback loop models that meet the changed goals. To demonstrate the applicability and effectiveness of the approach, we applied ActivFORMS in several domains: warehouse transportation, oceanic surveillance, tele assistance, and IoT building security monitoring.