Analysis and synthesis of distributed systems and protocols
Y. Yaw · 1987
In a distributed system, processes coordinate among themselves through interactions or communications. A set of rules (called protocols) is required to control how messages are exchanged among communication processes. The complexity of designing a distributed system grows rapidly as the number of entities and functions handled by the distributed system increase. This thesis proposes: (1) A Petri net reduction algorithm for protocol analysis, (2) A synthesis procedure for error-recoverable protocols, and (3) A design methodology for distributed system designs. These proposals reduce the complexity of design and analysis. This thesis presents a general Petri net reduction algorithm that reduces the number of states while preserving all desirable and undesirable properties. First, Dong's (DON 83) definition of (Well-Behaved Modules) WBMs to include more reducible subnets will be presented and extended. A WBM is a module that can be reduced while preserving some properties. A new concept of Simple Well-Behaved Modules (SWBMs) is introduced to automate reductions. Complicated WBMs can be reduced by recursively performing reductions of SWBMs. The problem is then reduced to finding conditions for SWBMs by progressing from simpler SWBMs to more complicated ones. Finally, the usefulness of this algorithm is demonstrated by applying it to the state exploration in protocol analysis. Other applications such as error detection, deadlock detection and prevention performance evaluation, and software engineering are also discussed. In the synthesis area, a correct, general, and efficient procedure has been developed for synthesizing two-party error-recoverable protocols for noisy channels where messages could be lost, corrupted, and/or missequenced. In this work, a new design methodology for distributed systems is presented which can also be applied to the synthesis of local entities. Also systems with more than two entities can be synthesized. The Petri net model is incrementally expanded by adding line elements according to the prescribed rules. These line elements are generated to increase the number of concurrent (subprocesses) processes, conditional (alternative) processes, and iterative (cyclic) processes. Another set of rules has been developed to assure the correct generation of these line elements. This approach will handle messages and internal interactions. Further, this approach is applicable to both local entity and multi-entity designs. (Abstract shortened with permission of author.)