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

TL;DR

This paper introduces a formal model combining Petri nets to improve decision-making in self-adaptive systems, ensuring quality objectives are met despite uncertainties.

Contribution

It presents a novel formal model that integrates high-level and plausible Petri nets for better decision-making in quality-driven self-adaptive systems under uncertainty.

Findings

Enhanced modeling of system quality attributes

Improved decision-making process under uncertainty

Formal guarantees on system behavior

Abstract

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.