Automated verification and refinement for physical-layer protocols

DOI10.1007/S00165-010-0149-0MaRDI QIDQ539420zbMATH OpenOpenAlexFDO

Authors Geoffrey M. Brown, Lee Pike

Publication date 30 May 2011

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

Full work available at URL https://doi.org/10.1007/s00165-010-0149-0

zbMATH Keywords

biphase markinfinite-state model checkingphysical layerreal-timesatisfiability modulo theories (SMT)UART

Mathematics Subject Classification ID

Network protocols (68M12) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Analysis of a biphase mark protocol with Uppaal and PVS
• Theory refinement for program verification
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• Verification of timed automata via satisfiability checking
• Verified model checking of timed automata

Cites work

• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• Analysis of a biphase mark protocol with Uppaal and PVS
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• scientific article; zbMATH DE number 1670798 (Why is no real title available?)
• scientific article; zbMATH DE number 1701759 (Why is no real title available?)
• scientific article; zbMATH DE number 1106375 (Why is no real title available?)
• scientific article; zbMATH DE number 2080768 (Why is no real title available?)
• The existence of refinement mappings

Cited in

(1)

• Analysis of a biphase mark protocol with Uppaal and PVS

Describes a project that uses

Uses Software

• Yices

This page was built for publication: Automated verification and refinement for physical-layer protocols

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