Model checking duration calculus: a practical approach
From MaRDI portal
Publication:939170
DOI10.1007/s00165-008-0082-7zbMath1151.68487OpenAlexW2138362538MaRDI QIDQ939170
Johannes Faber, Jochen Hoenicke, Andrey Rybalchenko, Roland Meyer
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
Real-time systemsModel checkingVerificationTimed automataDuration CalculusCase studyEuropean Train Control System
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Constraint solving for interpolation, A practical approach to model checking duration calculus using Presburger arithmetic, An abstract model for proving safety of autonomous urban traffic, Automatic Verification of Combined Specifications: An Overview
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A theory of timed automata
- The power of reachability testing for timed automata
- Duration calculus. A formal approach to real-time systems.
- Model-checking dense-time duration calculus
- Verification of concurrent programs: The automata-theoretic framework
- Interval Duration Logic
- Abstractions from proofs
- Model Checking Duration Calculus: A Practical Approach
- Slicing Concurrent Real-Time System Specifications for Verification
- Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters
- Transition predicate abstraction and fair termination
- Constructing Test Automata from Graphical Real-Time Requirements
- Differential Dynamic Logic for Verifying Parametric Hybrid Systems
- Constraint Solving for Interpolation
- FM 2005: Formal Methods
- Deciding an Interval Logic with Accumulated Durations
- Static Analysis
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Computer Aided Verification