College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
|Title: ||A Model and Temporal proof system for Networks of Processes|
|Authors: ||Nguyen, Van Long|
Demers, Alan J.
Owicki, Susan S.
|Keywords: ||computer science|
|Issue Date: ||Jun-1985|
|Publisher: ||Cornell University|
|Abstract: ||An approach is presented for modeling networks of processes that communicate exclusively through message passing. A process (or a network) is defined by its set of possible behaviors, where each behavior is an abstraction of an infinite execution sequence of the process. The resulting model is simple and modular and facilitates information hiding. It can describe both synchronous and asynchronous networks. It supports recursively-defined networks and can characterize liveness properties such as progress of inputs and outputs, termination, and deadlock. A sound and complete temporal proof system based on the model is presented. It is compositional - a specification of a network is formed naturally from specifications of its components.|
|Appears in Collections:||Computer Science Technical Reports|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.