Program Semantics, Specification and Verification: Theory and Applications. The conference materials
Conference proceedings (Nizhni Novgorod, Russia, July 1-2, 2012). Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceeding of the third workshop dedicaied to formalisms for program semantics, formal models and semantics of programs and systems, semantics of programming and specification languages, etc.
Nested Petri nets (NP-nets) are Petri nets with net tokens - an extension of high-level Petri nets for modeling active objects, mobility and dynamics in distributed systems. In this paper we present an algorithm for translating two-level NP-nets into behaviorally equivalent Colored Petri nets with the view of applying CPN methods and tools for nested Petri nets analysis. We prove, that the proposed translation preserves dynamic semantics in terms of bisimulation equivalence.