Towards integrated verification of timed transition models

MaRDI QIDQ5480168zbMATH OpenFDO

Authors Mark Lawford, Vera Pantelic, Hong Zhang

Publication date 26 July 2006

zbMATH Keywords

real-timemodel reductiontheorem provingmodel-checkingPVSSALequivalence verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 5181779
• Temporal proof methodologies for timed transition systems
• Verified model checking of timed automata
• An embedding of timed transition systems in \(HOL\)
• scientific article; zbMATH DE number 1507209

Cited in

(10)

• Proof assistance for real-time systems using an interactive theorem prover
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Verification of \(N\)-\(M\) switching control system: a case study in temporal logic model checking
• Verifying hierarchical Ptolemy II discrete-event models using real-time maude
• How to verify a Safe real-time system: The application of model checking and timed automata to the production cell case study
• Modeling and verification of real-time systems based on equations
• An embedding of timed transition systems in \(HOL\)
• Parametric Timed Model Checking for Guaranteeing Timed Opacity
• Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems
• Modeling Long–Running Transactions with Communicating Hierarchical Timed Automata

Describes a project that uses

Uses Software

• MOCHA
• Uppaal
• PVS

This page was built for publication: Towards integrated verification of timed transition models

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