Petri net modeling for reactive system verification
Bruno Blašković · 2003
Verification methodologies like model terms. However, there are also some diferrences. Rechecking and proving are part Of active system must respond to external stimuli within complex system design. Correc t behaviour of cans t ra in ts also t ime dependable. niand. On the other hand, Real Tzme System has the This paper sublimes modeling efforts in order t o bridge notion of time built in, like time supervisory controls. t h e g a p between concurrent software, model checking ~h~ development of a model checking input cade fro,,, butt,on that will (automatically?) find errors (like t h e formal specification or source code can produce hundeadlocks). and other non desired system's behaviour. current reactive real-time is among other con. given amollnt of t,ime, like responding on llser's d e Hypothetic goal is to provide designer with pushcomputations and formal ,. dreds lines of code. I n order to automat ize such a task, here int roduced as model extracting, t h e experimental meta-model ina framework i s developed to bridEe seThree mainstreart1 are possible regarding tlle details of design process: m a n t i d differences between various software verificaa) analysis: selected stages of development are examtian tools on one, and hetween system description on ined with appropriate tools. Speci&ed tools are t h e o t h e r side. Modeling an where the model checkers or theorem provers. Such design is model for experimenting wi th t h e problem solution i s also known as bottom-up approach. built. T h e model consists of interconnected Elemenb) synthesis: l ~ l ~ r e &tract representation is transformed in the target structure and code (the topt a r y Communicat ing Processes ( E C P ) . An interprotat ion of interconnections reflects the model of computareactive a u t o m a t a , component and coordinat ion modtarget, structure satisfies desired properties (no tion used: object oriented, Petri Net , communicat ing down approach). Synthesis process implies that ob, intelligent agents . . . E C P are grouped on th ree levels of abs t rac t ion to benefit f rom theoretical backgrounds like process algebras or high level P e t r i nets. Roughly speaking, model is t h e collection of connected tools a n d modeling i s ' the process of t h e tool integration. Fur ther on, after t h e presentat ion of some related approachcs, meta-modelling framework is int roduced through P e t r i ne t model toge ther wi th illustrative exKeywordReal-time system, model checking, P e t r i nets, Elementary Communicat ing Processes, ( C O ) ~ pe metamodel ing framework ample.