A Formal Model for Quality-Driven Decision Making in Self-Adaptive Systems

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.