Temporal Verification of Fault-Tolerant Protocols

DOI10.1007/978-3-642-00867-2_3MaRDI QIDQ3623816zbMATH OpenOpenAlexWikidataFDO

Authors

Publication date 24 April 2009

Published in Methods, Models and Tools for Fault Tolerance (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-00867-2_3

Mathematics Subject Classification ID

Reliability, testing and fault tolerance of networks and computer systems (68M15) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 1444728
• Reasoning about systems with many processes
• Program Development in Computational Logic
• Parameterized verification of leader/follower systems via first-order temporal logic

Cites work

• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1931652 (Why is no real title available?)
• scientific article; zbMATH DE number 2243382 (Why is no real title available?)
• An automatic abstraction technique for verifying featured, parameterised systems
• Automated Reasoning
• Axiomatizing the monodic fragment of first-order temporal logic
• Computer Aided Verification
• Constraint-based verification of parameterized cache coherence protocols
• Decidable fragments of first-order temporal logics
• Mechanising first-order temporal resolution
• Monodic temporal resolution
• Propositional temporal logics: decidability and completeness
• Proving Liveness by Backwards Reachability
• \textsc{tlpvs}: A \textsc{pvs}-based \textsc{ltl} verification system

Cited in

(4)

• Parameterized verification of leader/follower systems via first-order temporal logic
• scientific article; zbMATH DE number 1424027 (Why is no real title available?)
• Verification of distributed systems with the axiomatic system of MSVL
• Theoretical foundations of handling large substitution sets in temporal integrity monitoring

Describes a project that uses

Uses Software

• TLPVS
• TeMP
• PVS
• SPIN

This page was built for publication: Temporal Verification of Fault-Tolerant Protocols

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