Skip to main content


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

Please use this identifier to cite or link to this item:
Title: State Machines and Assertions (An Integrated Approach to Modelingand Verification of Distributed Systems
Authors: Joseph, Thomas A.
Raeuchle, Thomas
Toueg, Sam
Keywords: computer science
technical report
Issue Date: Nov-1985
Publisher: Cornell University
Abstract: This paper describes a methodology for modeling and verifying protocols for asynchronous message passing systems. It combines the techniques of finite state analysis and axiomatic verification. It overcomes the problem of state explosion by using variables and logical assertions where the finite state approach would require a large number of states. By explicitly including states where interactions between processes occur, the complexity of assertional proofs is significantly reduced. Properties like freedom from deadlock, freedom from unspecified message receptions, boundedness of channel size, and partial correctness can be proved. Properties of channels like losing or garbling messages can be modeled, as can premature and non-premature timeouts. The technique is illustrated by proving a sliding window flow control protocol and an alternating bit protocol that is correct only if timeouts are non-premature.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
85-652.pdf2.21 MBAdobe PDFView/Open
85-652.ps718.47 kBPostscriptView/Open

Refworks Export

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


© 2014 Cornell University Library Contact Us