Property-preserving Petri Net Process Algebra in Software Engineering

1. Introduction. 1.1. This book's approach for component-based system design. 1.2. Background information and main features of PPPA. 1.3. Organization of this book -- 2. Fundamentals on PPPA and related work. 2.1. Preliminaries and basic properties of petri nets. 2.2. General approaches for verification. 2.3. Related work and discussion -- 3. Petri net processes and extension operators. 3.1. The structure of a petri net process. 3.2. Structural properties of petri net processes. 3.3. Behavioral properties of petri net processes. 3.4. An example. 3.5. Notations for the description of PPPA. 3.6. The operator action prefix. 3.7. The operator BYPASS b|B. 3.8. The operator ITERATION B[symbol] -- 4. Composition operators of PPPA. 4.1. The operator ENABLE. 4.2. The operator CHOICE. 4.3. The operator INTERLEAVE. 4.4. The operator PARALLEL. 4.5. The operator DISABLE. 4.6. The operator DISABLE-RESUME -- 5. Property-preserving refinements. 5.1. A property-preserving refinement for transitions. 5.2. A property-preserving refinement for places. 5.3. An example for transformation TR -- 6. Property-preserving reductions. 6.1. Reducing a transition-bordered path to a transition. 6.2. Reducing a place-bordered path to a place. 6.3. Reducing a place-bordered subnet to a place. 6.4. Application examples -- 7. Place-merging operators for resource sharing. 7.1. Merging arbitrary sets of places. 7.2. Merging sets of non-neighboring places. 7.3. Composition via merging multiple pairs of places. 7.4. Composition via merging two single places. 7.5. Application -- 8. Application of PPPA to component-based design of manufacturing systems. 8.1. Background and motivation. 8.2. Summary of applying PPPA to component-based approach. 8.3. Application of PPPA to manufacturing system design -- 9. Application of PPPA to multi-agent system design. 9.1. Background and motivation. 9.2. PPPA-based methodology for designing multi-agent systems. 9.3. Verifying the MAS (step 3 described in section 9.2.1). 9.4. Remarks -- 10. Application of PPPA to job-shop scheduling systems. 10.1. Background and motivation. 10.2. JSS system design and Makespan calculation. 10.3. JSS design and optimization - A case study -- 11. Application of PPPA to security policy design. 11.1. Background and motivation. 11.2. Related work. 11.3. Petri net-based properties for security policy. 11.4. Modular policy composition based on EPNP. 11.5. EPNP-based specification of XACML combiners. 11.6. A large scale complex policy design - A case study. 11.7. Conclusive remarks