Disputation i data- och informationsvetenskap: Muhammad Usman Iftikhar
Titel: En modellbaserad metod för att utveckla självadaptiva system med garantier
Ämne: Data- och informationsvetenskap
Fakultet: Fakulteten för teknik
Datum: Måndagen den 18 december 2017 kl 13.15
Plats: Sal C1202 (Newton), hus C, Växjö
Opponent: Professor Flavio Oquendo, Université Bretagne Sud, Frankrike
Betygsnämnd: Docent Patrizio Pelliccione, Göteborgs universitet; docent Romina Spalazzese, Malmö högskola; professor Danny Hughes, KU Leuven, Belgien
Examinator: Professor Welf Löwe, Institutionen för datavetenskap, Linnéuniversitetet
Handledare: Professor Danny Weyns, Institutionen för datavetenskap, Linnéuniversitetet
Ordförande: Docent Jonas Lundberg, Institutionen för datavetenskap, Linnéuniversitetet
Spikning: Fredagen den 1 december 2017 kl 14.00, universitetsbiblioteket i Växjö
Abstract
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.