Danny Weyns is a professor at the Department of Computer Science of the Katholieke Universiteit Leuven, where he is with the imec-DistriNet reearch group. His main research interests are in software engineering of self-adaptive systems. Self-adaptation equips a software system with a feedback loop system that enables the system to deal operating conditions that are difficult to anticipate before deployment, such as uncertainty about the availability of resources and changing user goals. Danny’s current research focus is on the study of modelling and verification techniques that are applied at runtime to provide assurances for the required adaptation goals. His research team is particularly interested in decentralized systems, where adaptation needs to be realized by multiple feedback loops. The Internet of Things is an important domain where the research results are validated. Danny is also partime affiliated with Linnaeus University Sweden.
Title
Engineering self-adaptive systems with ActivFORMS
Abstract
An increasingly important challenge for software engineers is handling change. Our focus is on change caused by uncertainties in the operating conditions of a system that are very difficult to be predict before deployment. Examples are sudden changes in the environment in which the system operates, dynamics in the availability of resources that are required by the system, and user goals that change over time. To deal with such uncertainties, an external feedback loop can be added to the system that collects additional data during operation to resolve the uncertainties and uses the knowledge to adapt the system in order to achieve a set of adaptation goals (e.g., efficiency and reliability goals) regardless of the uncertainties. This approach is commonly referred to as self-adaptation. To ensure that the self-adaptive system complies with the adaptation goals, recent research suggests the use of formal techniques at runtime. However, several open challenges have not been solved yet, limiting the practical applicability of existing approaches. In particular, the need to: (i) provide guarantees for correct behavior of the feedback loop, (ii) enable efficient verification in terms of required time and resources to guarantee the adaption goals, and (iii) support changing adaptation goals at runtime. We present ActivFORMS (Active FORmal Models for Self-adaptation), a formally founded model-based approach for engineering self-adaptive systems that aims to contribute tacking these challenges. ActivFORMS provides: (i) guarantees for the correct behavior of the feedback loop with respect to a set of properties by using direct execution of verified models of the feedback loop, (ii) efficient guarantees for the adaption goals with a required accuracy and confidence by using statistical model checking techniques at runtime, and (iii) basic support for on the fly changing adaptation goals and updating verified models of the feedback loop that meet the new goals. We applied ActivFORMS to a real world IoT application for building security monitoring deployed at KU Leuven. The experimental results demonstrate that ActivFORMS can be used to engineer self-adaptive systems with guarantees.