Formal Specification and Verification of Distributed System.
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 of each other, and the entire system may lack an accurate global clock. In this thesis, we develop an event-based model to specify formally the behavior (the external view) and the structure (the internal view) of distributed systems. 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' relations, representing causality. No assumption about the existence of a global clock is made in the specifications.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1983
- Accession Number
- ADA139305
Entities
People
- B. S. Chen
- R. T. Yeh
Organizations
- University of Maryland