Towards integrated verification of timed transition models

MaRDI QIDQ5480168zbMATH OpenFDO

Authors Mark Lawford, Vera Pantelic, Hong Zhang

Publication date 26 July 2006

zbMATH Keywords

equivalence verificationmodel reductionmodel-checkingPVSreal-timeSALtheorem proving

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

(11)

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

Describes a project that uses

Uses Software

• PVS
• Uppaal
• MOCHA

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)