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
      Computer Hardware
      Computer Systems

Distribution Statement : APPROVED FOR PUBLIC RELEASE