Model checking duration calculus: a practical approach

DOI10.1007/S00165-008-0082-7MaRDI QIDQ939170zbMATH OpenOpenAlexFDO

Authors Roland Meyer, Johannes Faber, Jochen Hoenicke, Andrey Rybalchenko

Publication date 21 August 2008

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

Full work available at URL https://doi.org/10.1007/s00165-008-0082-7

zbMATH Keywords

Model checkingVerificationReal-time systemsTimed automataDuration CalculusCase studyEuropean Train Control System

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model Checking Duration Calculus: A Practical Approach
• Model-checking discrete duration calculus
• Checking temporal duration properties of timed automata.
• Verifying continuous-time duration calculus against real-time automaton
• Model-checking dense-time duration calculus

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 512815 (Why is no real title available?)
• scientific article; zbMATH DE number 2143088 (Why is no real title available?)
• scientific article; zbMATH DE number 1409638 (Why is no real title available?)
• A theory of timed automata
• Abstractions from proofs
• Constraint Solving for Interpolation
• Constructing test automata from graphical real-time requirements
• Deciding an Interval Logic with Accumulated Durations
• Differential Dynamic Logic for Verifying Parametric Hybrid Systems
• Duration calculus. A formal approach to real-time systems.
• FM 2005: Formal Methods
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Interpolation and SAT-based model checking.
• Interval duration logic: expressiveness and decidability
• Model Checking Duration Calculus: A Practical Approach
• Model-checking dense-time duration calculus
• Slicing Concurrent Real-Time System Specifications for Verification
• Static Analysis
• The power of reachability testing for timed automata
• Transition predicate abstraction and fair termination
• Verification of concurrent programs: The automata-theoretic framework
• Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters

Cited in

(14)

• A practical approach to model checking duration calculus using Presburger arithmetic
• Advances in model checking of extended linear duration invariants
• Model Checking Duration Calculus: A Practical Approach
• Take It NP-Easy: Bounded Model Construction for Duration Calculus
• Constraint solving for interpolation
• scientific article; zbMATH DE number 1956586 (Why is no real title available?)
• An abstract model for proving safety of autonomous urban traffic
• scientific article; zbMATH DE number 2087436 (Why is no real title available?)
• Model-checking discrete duration calculus
• FM 2005: Formal Methods
• scientific article; zbMATH DE number 2165695 (Why is no real title available?)
• Verifying continuous-time duration calculus against real-time automaton
• scientific article; zbMATH DE number 2038900 (Why is no real title available?)
• Automatic verification of combined specifications: an overview

Describes a project that uses

Uses Software

• IDLVALID
• ARMC
• Uppaal
• HyTech
• MoDeST

This page was built for publication: Model checking duration calculus: a practical approach

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