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/6489
Title: A Model and Temporal Proof System for Networks of Processes
Authors: Nguyen, Van Long
Gries, David
Owicki, Susan S.
Keywords: computer science
technical report
Issue Date: Nov-1984
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR84-651
Abstract: A model and a sound and complete proof system for networks of processes in which component processes communicate exclusively through messages is given. The model, an extension of the trace model, can desribe both synchronous and asynchronous networks. The proof system uses temporal-logic assertions on sequences of observations - a generalization of traces. The use of observations (traces) makes the proof system simple, compositional and modular, since internal details can be hidden. The expressive power of temporal logic makes it possible to prove temporal properties (safety, liveness, precedence, etc.) in the system. The proof system is language-independent and works for both synchronous and asynchronous networks.
URI: http://hdl.handle.net/1813/6489
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
84-651.pdf2.35 MBAdobe PDFView/Open
84-651.ps1.11 MBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us