Compositional verification of a communication protocol for a remotely operated aircraft

DOI10.1016/J.SCICO.2011.10.011MaRDI QIDQ2442952zbMATH OpenOpenAlexFDO

Authors Alwyn E. Goodloe, César Muñoz

Publication date 2 April 2014

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

Full work available at URL https://doi.org/10.1016/j.scico.2011.10.011

zbMATH Keywords

compositional reasoninginteractive theorem provingprotocol verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Mechanizing a process algebra for network protocols
• Specification and verification of the classical sliding window protocol
• scientific article; zbMATH DE number 1424027
• Verifying Communication Protocols Using Live Sequence Chart Specifications
• A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol

Cites work

• A Marriage of Rely/Guarantee and Separation Logic
• Algebraic Specification of Communication Protocols
• An axiomatic proof technique for parallel programs
• An incremental specification of the sliding-window protocol
• Composing invariants
• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• scientific article; zbMATH DE number 1956576 (Why is no real title available?)
• Tentative steps toward a development method for interfering programs
• The Rely-Guarantee method for verifying shared variable concurrent programs
• The sliding-window protocol revisited
• Three snippets of curve evolution theory in computer vision
• Verification of a sliding window protocol in \(\mu\) CRL and PVS

Cited in

(7)

• Formal analysis of the application programming interface of the PVS verification system
• Mechanizing a process algebra for network protocols
• Log your car: reliable maintenance services record
• scientific article; zbMATH DE number 2086997 (Why is no real title available?)
• scientific article; zbMATH DE number 1424027 (Why is no real title available?)
• Theorem Proving in Higher Order Logics
• When human intuition fails: using formal methods to find an error in the ``proof of a multi-agent protocol

Describes a project that uses

Uses Software

• SPIN
• PVS

This page was built for publication: Compositional verification of a communication protocol for a remotely operated aircraft

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