Formal Modeling of Evolving Systems using Petri nets Based Vocabulary

Abstract

In this research we proposed a Petri nets based vocabulary for the development of self adaptive systems. Self adaptive systems (SAS) are systems that undergo dynamicity by reconfiguring their behaviors in accordance with the system needs for execution of programs. Self adaptation has become building block for developing computer systems as it make systems work with higher precision, validity reliability with minimal human effort. Idea behind self adaptation is to enable systems to overcome runtime issues with no or minimal human intervention. SAS consists of two subsystems, a managed system and a self-adaptive system that works as feedback loop. In our approach we used MAPE-K feedback loop that comprises on components monitor, analyze, plan, execute and knowledge to perform self-adaptation. Formal verification of self adaptive systems can be done by specifying actions to be performed by evolving systems. A model is proposed to formally express self adaptive systems. For Formal specification of Evolving systems we have used Linear Temporal Logic (LTL) for the formalism as LTL provides high level of understandability with less ambiguous nature. Verification of system properties have been done using SPIN model checker environment.