Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6530
Title: A Model and Temporal proof system for Networks of Processes
Authors: Nguyen, Van Long
Demers, Alan J.
Gries, David
Owicki, Susan S.
Keywords: computer science
technical report
Issue Date: Jun-1985
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR85-690
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.
URI: http://hdl.handle.net/1813/6530
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
85-690.pdf3.15 MBAdobe PDFView/Open
85-690.ps1.08 MBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us