@InBook{Camara/2016/SMGs,
AUTHOR = {C\'{a}mara, Javier and Garlan, David and Moreno, Gabriel A. and Schmerl, Bradley},
TITLE = {Analyzing Self-Adaptation via Model Checking of Stochastic Games},
YEAR = {2017},
BOOKTITLE = {Software Engineering for Self-Adaptive Systems III. Assurances},
NUMBER = {9640},
EDITOR = {de Lemos, Rog\'{e}rio and Garlan, David and Ghezzi, Carlo and Giese, Holger},
PUBLISHER = {Springer},
TYPE = {Lecture Notes in Computer Science},
PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/SEfSAS3-SMGs.pdf},
ABSTRACT = {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}
}
|
|
