Event-Based Specification and Verification of Distributed Systems.
Abstract
Computations of distributed systems are extremely difficult to specify and verify using traditional techniques because the systems are inherently concurrent, asynchronous and nondeterministic. Furthermore, computing nodes in a distributed system may be highly independent, and the entire system may lack an accurate global clock. In this thesis, the author develops an event-based model to specify formally the behavior (the external view) and the structure (the internal view) of distributed systems. The specification technique has a rather wide range of applications. Examples from different classes of distributed systems, including communication systems, transaction-based systems and process control systems are demonstrated. Both control-related and data-related properties of distributed systems are specified using two fundamental relationships among events: the precedes relation, representing time order; and the enables relation, representing causality. No assumption about the existence of a global clock is made in the specifications. The correctness of a design can be proved before implementation by checking the consistency between the behavior specification and structure specification of a system. Moreover, since the specification technique defines the orthogonal properties of a system separately, each of them can then be verified independently. Thus, the proof technique avoids the exponential state-explosion problem found in state-machine specification techniques.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1982
- Accession Number
- ADA128629
Entities
People
- Bo-shoe Chen
Organizations
- University of Maryland