engleski

Petri Net Modeling for Reactive System Verification

Verification methodologies like model checking and theorem proving are important part of complex system design. Correct behaviour of concurrent reactive real-time system is among other constraints also time dependable. This paper sublimes modeling efforts in order to bridge the gap between concurrent software, model checking tools, models of computations and formal specifications. The development of a model checking input code from the formal specification or source code can produce hundreds lines of code. In order to automatize such a task, here introduced as model extracting, the experimental meta-modeling framework is developed to bridge semantical differences between various software verification tools on one, and between system description on the other side. Modeling framework is an environment where the model for experimenting with the problem solution is built. The model consists of interconnected Elementary Communicating Processes (ECP). An interpretation of interconnections reflects the model of computation used: object oriented, Petri Net, communicating reactive automata, component and coordination models, intelligent agents ... ECP are grouped on three levels of abstraction to benefit from theoretical backgrounds like process algebras or high level Petri nets. Roughly speaking, model is the collection of connected tools and modeling is the proces of tool integration. Further on, after the presentation of some related approaches, meta-modelling framework is introduced through Petri net model together with illustrative example.

Real-time system; model checking; Petri nets; Elementary Communicating Processes; CO4pe metamodeling framework

nije evidentirano