PROPERTY-PRESERVING PETRI NET PROCESS ALGEBRA IN SOFTWARE ENGINEERING
Hejiao Huang, Li Jiao, To-Yat Cheung
This book presents a component -based methodology for the creation and verification of design specifications. The methodology is formally presented as an algebra called Property-Preserving Petri Net Process Algebra (PPPA). PPPA includes five classes of operators, and the authors show that every operator of PPPA can preserve a large number of basic system properties. Therefore, if the initial set of primitive components satisfies some of these properties, the created components will also "automatically" satisfy them without the need for further verification - thus greatly saving verification efforts.