Multi-formalism Based Specification Language: Syntax, Semantics, Verification and Simulation

Abstract—This work presents a specification language called PNOZ, based on two formalisms: Petri Nets and Object-Z. Such a specification style facilitates the modeling of systems with compartmental and functional aspects. The accent is placed on PNOZ semantics so as to give formal foundations to the validation and simulation of models based in this heterogeneous language. Every PNOZ model has a transition system as its semantic interpretation. Precisely, we will be interested to stochastic version of the PNOZ semantic. Transition system model of a PNOZ class can be used for verification purposes by model checking. A real-word example is treated and the resulting specification is model-checked by using the Symbolic Analysis Laboratory (SAL)