Verifying Stochastic Behaviors of Decentralized Self-Adaptive Systems: A Formal Modeling and Simulation Based Approach

TL;DR

This paper presents a formal modeling and simulation approach using timed automata and logic to verify the stochastic behaviors of decentralized self-adaptive systems, demonstrated through UAV emergency scenarios.

Contribution

It introduces a combined formal modeling and simulation framework for analyzing and verifying decentralized self-adaptive systems in dynamic environments.

Findings

Verified adaptation properties through stochastic simulations

Demonstrated approach effectiveness with UAV emergency scenario

Provided statistical results for UAV arrangement planning

Abstract

Self-adaptive software is considered as the most advanced approach and its development attracts a lot of attention. Decentralization is an effective way to design and manage the complexity of modern self-adaptive software systems. However, there are still tremendous challenges. One major challenge is to unify decentrality with traditional self-adaptive implementation framework during design and implementation activity. One is to guarantee the required global goals and performance of decentralized self-adaptive systems operating in highly dynamic and uncertain environments. Another challenge is to predict the influence of system's internal change on its self-adaptability to the environment. To solve these problems, we combine the mechanisms of separation of concerns with modeling method using timed automata to allow the system to be analyzed and verified. Timed computation tree logic is used to specify system goals and stochastic simulations in dynamic environment are experimented to verify decentralized self-adaptive system's adaptation properties. In this paper, we extracted a motivation example from practical applications in UAV emergency mission scenarios. The whole approach is evaluated and illustrated with this motivation example and the statistical results can be used as reference for arrangement planning of UAVs in cyber physical spaces.