Modelling of distributed programming systems with using of property-preserving Petri net process algebras and P/T Petri net processes

Petri nets represent popular formalism and methodology for the design and development of all kind of parallel or concurrent systems. Property-preserving Petri net process algebras (PPPA) were originally designed for the specification and verification of the manufacturing systems. The elements of PPPA are the Petri net processes and among other features PPPA does not need to verify composition of the Petri net processes because all their algebraic operators preserve the specified set of the properties. These original PPPA are generalized for the newly introduced class of the P/T Petri nets processes, additional PPPA composition operator SYNC-CALL is defined and its chosen properties are proved in this article. The PPPA can be then with the support of the SYNC-CALL operator easily extended also into the area of design, simulation and verification of multithreading programming systems executed in parallel or distributed environment and based on the object-oriented programming paradigma.