A Formal Model for Quality-Driven Decision Making in Self-Adaptive Systems
This work aims to provide a rigorous definition and analysis of system behavioral properties for self-adaptive systems, which is an incremental improvement for researchers and practitioners in the field of formal methods for adaptive systems.
This paper addresses the challenge of maintaining quality of service in self-adaptive systems under uncertainty. It proposes a formal model that combines high-level Petri nets and plausible Petri nets to quantify system quality attributes and improve decision-making by selecting the most plausible plans based on the system's context.
Maintaining an acceptable level of quality of service in modern complex systems is challenging, particularly in the presence of various forms of uncertainty caused by changing execution context, unpredicted events, etc. Although self-adaptability is a well-established approach for modelling such systems, and thus enabling them to achieve functional and/or quality of service objectives by autonomously modifying their behavior at runtime, guaranteeing a continuous satisfaction of quality objectives is still challenging and needs a rigorous definition and analysis of system behavioral properties. Formal methods constitute a promising and effective solution in this direction in order to rigorously specify mathematical models of a software system and to analyze its behavior. They are also largely adopted to analyze and provide guarantees on the required functional/non-functional properties of self-adaptive systems. Therefore, we introduce a formal model for quality-driven self-adaptive systems under uncertainty. We combine high-level Petri nets and plausible Petri nets in order to model complex data structures enabling system quality attributes quantification and to improve the decision-making process through selecting the most plausible plans with regard to the system's actual context.