Analysis of a biphase mark protocol with Uppaal and PVS

DOI10.1007/S00165-006-0008-1MaRDI QIDQ855013zbMATH OpenOpenAlexFDO

Authors A. L. de Groot, F. Vaandrager

Publication date 20 December 2006

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

Full work available at URL http://hdl.handle.net/2066/36086

zbMATH Keywords

Model checkingFormal methodsTimed automataBiphase mark protocolTheorem provers

Mathematics Subject Classification ID

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

Recommendations

• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• Automated verification of an audio-control protocol using UPPAAL
• Automatic verification of a lip-synchronisation protocol using UPPAAL
• Automated verification and refinement for physical-layer protocols
• scientific article; zbMATH DE number 3892605

Cites work

• scientific article; zbMATH DE number 1617317 (Why is no real title available?)
• scientific article; zbMATH DE number 1670792 (Why is no real title available?)
• scientific article; zbMATH DE number 1956576 (Why is no real title available?)
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• A theory of timed automata
• Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
• Linear parametric model checking of timed automata
• Probabilistic clock synchronization
• Uppaal in a nutshell

Cited in

(5)

• Automated verification and refinement for physical-layer protocols
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• A compositional translation of timed automata with deadlines to Uppaal timed automata
• Analysis of a clock synchronization protocol for wireless sensor networks
• Model-checking timed automata with deadlines with Uppaal

Describes a project that uses

Uses Software

• NQTHM
• Uppaal
• PVS
• Kronos

This page was built for publication: Analysis of a biphase mark protocol with Uppaal and PVS

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