Back to Search
Start Over
Formal Specification and Verification of Distributed Systems.
- Source :
- IEEE Transactions on Software Engineering; Nov83, Vol. 9 Issue 6, p710-722, 13p, 2 Color Photographs, 12 Diagrams
- Publication Year :
- 1983
-
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 paper, 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. The specification technique has a rather wide range of applications. Examples from different classes of distributed systems, include communication systems, process control systems, and a distributed prime number generator, are used to demonstrate the power of the technique. The correctness of a design can be proved before implementation by checking the consistency between the behavior specification and the structure specification of a system. Both safety and liveness properties can be specified and verified. Furthermore, 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. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 00985589
- Volume :
- 9
- Issue :
- 6
- Database :
- Complementary Index
- Journal :
- IEEE Transactions on Software Engineering
- Publication Type :
- Academic Journal
- Accession number :
- 14370440