Formal Specification and Verification of Self-Adaptive Concurrent Systems

Abstract

The assurance of required quality properties is one of the major challenges in self-adaptive systems (SASs). SASs have the capability to adapt their dynamic behavior autonomously at runtime due to uncertain changes in the environment. In general, an SAS is much difficult to specify and verify, because of its highly complex internal behavior and especially when time constraints are involved. In this research, we use modal μ-calculus (Mμ) for the specification and verification of colored Petri nets-based self-adaptive concurrent systems. We propose self-adaptive multi-agent concurrent system (SMACS) framework that is specifically designed for complex architectures. The internal structure of SMACS framework is based on MAPE-K feedback loop. Each phase of the feedback loop works as an internal agent (Int-Agent) known as Monitor Int-Agent, Analyzer Int-Agent, Planer Int-Agent, and Executer Int-Agent. The decentralized approach is being used in this research, and due to this approach, all agents intelligently adapt their behavior in the environment and send updates to other agents. For verification of internal properties like liveness, safeness, and deadlock-freedom of each agent, the TAPA model checker is being used. For the implementation of SMACS framework, traffic monitoring system is chosen as a case study.

Keywords

• Self-adaptive
• multi-agent
• formal specification
• formal verification
• μ-calculus%22%2C%22default_operator%22%3A%22AND%22%7D%7D%7D"> modal <italic xmlns:ali="http://www.niso.org/schemas/ali/1.0/" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">μ</italic>-calculus
• TAPA model checker