A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol

DOI10.1007/BF01211081zbMath0802.68006OpenAlexW2122645481MaRDI QIDQ1318283

J. Strother Moore

Publication date: 27 March 1994

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01211081

zbMATH Keywords

fault tolerancehardware verificationclock synchronizationautomatic theorem provingperformance modelingprotocol verificationBoyer-Moore logicISO protocol level 1manchester format

Mathematics Subject Classification ID

Communication networks in operations research (90B18) Network design and communication in computer systems (68M10) Mathematical problems of computer architecture (68M07)

Related Items (6)

Analysis of a biphase mark protocol with Uppaal and PVS ⋮ Wait-free linearization with a mechanical proof ⋮ A functional formalization of on chip communications ⋮ Automated verification and refinement for physical-layer protocols ⋮ Theories for mechanical proofs of imperative programs ⋮ A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol

Uses Software

• NQTHM
• UNITY

Cites Work

• Adequate proof principles for invariance and liveness properties of concurrent programs
• A survey of verification techniques for parallel programs
• A calculus of communicating systems
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• FM8501: a verified microprocessor
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Reaching Agreement in the Presence of Faults
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol