Petri Nets Based Formal Modeling and Verification of Concurrent Systems

Abstract

The assurance of required quality properties is one of the major challenge in Self- Adaptive Systems (SAS). Self-adaptive systems have the capability to adapt their dynamic behavior autonomously at runtime due to uncertain changes in the environment. Research in this field is being held since mid-sixties, and over the last decade the importance of self-adaptivity is being increased. In general a self-adaptive system is much difficult to specify and verify, because of its highly complex internal behavior and especially when time constraints are involved. In the proposed research, Colored Petri Net (CPN) formal language will be used to model self-adaptive multi-agent system. CPN is increasingly used to model self-adaptive complex concurrent systems due to its flexible formal specification and formal verification behavior. CPN is visually more expressive than simple Petri Nets enables diverse modeling approaches and provides a richer framework for such a complex formalism. The specification and verification of internal structure of each self-adaptive agent is being expressed through modal μ-calculus (Mμ). We propose SMACS (Self-adaptive Multi-Agent Concurrent System) framework, that is specifically designed for complex architectures, those contain inter-connected components in a heterogenous way. All agents of SMACS are also known as intelligent agents due to their self-adaptation behavior. The internal structure of SMACS framework is based on MAPE-K feedback loop. Each phase of the feedback loop works as an internal agent known as; Monitor Int-Agent, Analyzer Int-Agent, Planer Int-Agent and Executer Int-Agent. The agents adapt and update their behavior through interaction with the environment by using the decentralized approach. The Liveness, Safeness and Deadlock-freedom properties of self-adaptive agents are being verified through the TAPA model checker. For implementation of SMACS framework, Traffic Monitoring System (TMS) and Smart Computer Lab (SCL) are chosen as case studies. CPN based state space analysis will also be done to verify the behavioral properties of the model. The general objective of the proposed system is to maximize the utility generated over some predetermined time horizon. This research will provide new direction for modeling and verification of concurrent system. The main idea behind this work is to achieve true concurrency of multiple interconnected self-adaptive agents with their dynamic behavior.