Contents -- Preface -- 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.2.1 Verification via reachability analysis -- 2.2.2 Verification via characterizations or problem conversion -- 2.2.3 Verification via property-preserving transformations -- 2.3 Related Work and Discussion -- 2.3.1 Reviews on property-preserving refinements for Petri nets -- 2.3.2 Reviews on property-preserving reductions for Petri nets -- 2.3.3 Reviews on property-preserving compositions for Petri nets -- 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

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 -- 8.3.1 Creating the primitive modules -- 8.3.2 Creating the system model -- 8.3.3 Verifying the system model -- 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.2.1 Summary of our methodology for designing MAS -- 9.2.2 Specifying the modules as Petri net processes (Substep 1.1 in Section 9.2.1) -- 9.2.3 Integrating the modules of the CLINIC (Substep 1.2 in Section 9.2.1) -- 9.2.4 Specification of the entire MAS (Step 2 described in Section 9.2.1) -- 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 -- 10.3.1 System design -- 10.3.2 Scheduling optimization -- 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.3.1 Completeness -- 11.3.2 Termination -- 11.3.3 Consistency -- 11.3.4 Confluence -- 11.4 Modular Policy Composition Based on EPNP -- 11.4.1 Logic-based operators for composition -- 11.4.2 Policy composition via resources sharing -- 11.4.3 Policy composition via operation synchronization -- 11.4.4 Policy refinement -- 11.5 EPNP-Based Specification of XACML Combiners -- 11.6 A Large Scale Complex Policy Design A Case Study -- 11.6.1 Specification of primitive modules.

11.6.2 Composition of sub-policies -- 11.6.3 Local policy specification and verification -- 11.6.4 Global policy specification and verification -- 11.7 Conclusive Remarks -- Bibliography.