Formal Verification of Distributed Self-Adaptive Systems Under Environmental Uncertainty

Distributed self-adaptive system is a multi-component collaborative system that automatically adjusts its behavior and structure through adaptive mechanisms to maintain system performance and stability in dynamic environments. The adaptability and robustness of these systems depend on the correctness of self-adaptive decisions in real-world scenarios. However, environmental uncertainty makes it difficult for the systems to accurately perceive their operating environments, which may result in misjudgments and consequently erroneous self-adaptive decisions. To address this issue, we propose a Stochastic Timed Automata-based Adaptive Verification method. By collecting data during system operation and using Bayesian methods to transform it into transition probabilities between system states, a stochastic timed automata model is constructed to simulate the system's operational process. Key properties are verified using statistical model checking to ensure the correctness of self-adaptive decisions. The effectiveness and efficiency of the method are demonstrated by verifying the adaptability and robustness of a multi-roadside unit collaborative system in intelligent transportation vehicle-road coordination.