In the past, there existed in the literature many techniques of applying Petri nets to system design. However, overall, these techniques were essentially independent and fragmentary and cannot be assembled together to form a satisfactory component-based approach for such a purpose. This thesis has two parts of contributions towards component-based system design. Part I enhances an existing incomplete algebra called Property-Preserving Petri Net Process Algebra (PPPA) by adding three sets of operators to it: 1) operators for refinement - including place-refinement and transition refinement; 2) operators for reduction - including reducing place-bordered path, reducing transition-bordered path and reducing place-bordered subnet; and 3) operators for place-merging – including merging an arbitrary set of places, merging a set of non-neighboring places, composition via merging pairs of places and composition via merging two single places. Based on PPPA, Part II of this thesis provides a self-contained component-based approach to system design in two areas of real-life applications, namely, manufacturing systems and multi-agent systems. The motivation and significance of our contributions may be understood in three aspects: (1) In a component-based approach for system specification, one needs a versatile structure for specifying the components and a closed set of operators for creating new components. Existing PPPA-based methods are highly inadequate for these purposes. What are available include only a partial set of operators mainly for the composition of components, such as Iteration, Enable, Choice, Interleave, Parallel, Disable, etc. The addition of new operators as presented in Part I of this thesis makes PPPA become a close and complete model for the specification and creation of components. (2) In a component-based approach for system verification, two of the main difficulties are: How to prove the correctness of the newly-created components if the original components are already correct and how to resolve the errors induced if the components to be integrated share some resources. Existing PPPA-based methods for these purposes are fragmentary and mostly unrelated. We resolve these problems by requiring the operators we propose to preserve more than nineteen system properties of the original components in the created components. The properties include: state machine, marked graph, free choice net, asymmetric choice net, conservativeness, structural boundedness, consistence, repetitiveness, rank, cluster, rank-cluster-property, coverability by minimal state-machines, siphon, trap, cyclomatic complexity, longest path, boundedness, liveness, reversibility and rank theorem. As a result, the newly-created components are automatically correct and no new efforts in verification are necessary. (3) Though the application of Petri nets in the design of manufacturing systems and multi-agent systems has begun more than a decade ago, the existing methodologies are essentially for individual problems and not adequate to form a component-based approach of system design. One of the well-known difficulties in these two areas of design is due to the frequent occurrence of resource sharing in the systems’ components. Based on PPPA, Part II of this thesis proposes a systematic component-based approach for their specification and verification and resolving part of these resource-sharing problems. Keywords: manufacturing system, multi-agent system, Petri net, process algebra, property-preserving, specification, system design, verification.
| Date of Award | 15 Jul 2004 |
|---|
| Original language | English |
|---|
| Awarding Institution | - City University of Hong Kong
|
|---|
| Supervisor | Xiaohua JIA (Supervisor) & To Yat CHEUNG (Supervisor) |
|---|