Use of eCommons for rapid dissemination of COVID-19 research
In order to maximize the discoverability of COVID-19 research, and to conform with repository best practices and the requirements of publishers and research funders, we provide special guidance for COVID-19 submissions.
State Machines and Assertions (An Integrated Approach to Modelingand Verification of Distributed Systems
|dc.contributor.author||Joseph, Thomas A.||en_US|
|dc.description.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.||en_US|
|dc.title||State Machines and Assertions (An Integrated Approach to Modelingand Verification of Distributed Systems||en_US|