Accession Number : ADA139305
Title : Formal Specification and Verification of Distributed System.
Descriptive Note : Technical rept.,
Corporate Author : MARYLAND UNIV COLLEGE PARK DEPT OF COMPUTER SCIENCE
Personal Author(s) : Chen,B S ; Yeh,R T
PDF Url : ADA139305
Report Date : Jun 1983
Pagination or Media Count : 49
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.
Descriptors : *Distributed data processing, *Computers, *Systems engineering, Data transmission systems, Performance(Engineering), Computer architecture, Message processing, Computations, Specifications, Validation, Models, Interfaces, Programming languages, Communications networks
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE