|Analyzing Self-Adaptation via Model Checking of Stochastic Games|
Gabriel A. Moreno and
In Rogério de Lemos,
David Garlan, Carlo Ghezzi and Holger Giese editors, Software Engineering for Self-Adaptive Systems III. Assurances, Nr. (9640), Lecture Notes in Computer Science, Springer, 2017.
Online links: Plain Text
|Design decisions made during early development stages of self-adaptive systems tend to have a significant impact upon system properties at runtime
(e.g., safety, QoS). However, understanding the implications of these decisions
a priori is difficult due to the different types and degrees of uncertainty that affect such systems (e.g., simplifying assumptions, human-in-the-loop). To provide
some assurances about self-adaptive system designs, evidence can be gathered
from activities such as simulations and prototyping, but these demand a significant effort and do not provide a systematic way of dealing with uncertainty. In this chapter, we describe an approach based on model checking of stochastic multiplayer games (SMGs) that enables developers to approximate the behavioral envelope of a self-adaptive system by analyzing best- and worst-case scenarios of alternative designs for self-adaptation mechanisms. Compared to other sources of evidence, such as simulations or prototypes, our approach provides developers with a preliminary understanding of adaptation behavior with less effort, and without the need to have any specific adaptation algorithms or infrastructure in place. We illustrate our approach by showing how it can be used to mitigate different types of uncertainty in contexts such as self-protecting systems, proactive
latency-aware adaptation, and human-in-the-loop.|
Keywords: Assurance, Formal Methods, Human-in-the-loop, Model Checking, Science of Security, Self-adaptation, Stochastic Games.