State machines and assertions: An integrated approach to modeling and verification of distributed systems

DOI10.1016/0167-6423(86)90002-XMaRDI QIDQ1077153zbMATH OpenOpenAlexFDO

Authors Thomas A. Joseph, Thomas Räuchle, Sam Toueg

Publication date 1986

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(86)90002-x

zbMATH Keywords

alternating bit protocolassertional proofsaxiomatic verificationboundedness of channel sizedeadlockfinite state analysispartial correctnessprotocols for asynchronous message passing systemsunspecified message receptionswindow flow control protocol

Mathematics Subject Classification ID

Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 4119602
• On "A Simple Protocol Whose Proof Isńt": The State Machine Approach
• Verification of distributed systems with local-global predicates
• Verifying the correctness of distributed systems via mergeable parallelism
• scientific article; zbMATH DE number 2080915

Cited in

(2)

• Exposure to deadlock for communicating processes is hard to detect
• scientific article; zbMATH DE number 2084333 (Why is no real title available?)

This page was built for publication: State machines and assertions: An integrated approach to modeling and verification of distributed systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1077153)