Kronos: A verification tool for real-time systems
From MaRDI portal
Publication:1856194
DOI10.1007/S100090050009zbMath1060.68606OpenAlexW2023499821MaRDI QIDQ1856194
Publication date: 1997
Published in: International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s100090050009
Related Items (66)
Timed recursive state machines: expressiveness and complexity ⋮ Presburger liveness verification of discrete timed automata. ⋮ Explaining safety violations in real-time systems ⋮ Scheduling with timed automata ⋮ Updatable timed automata ⋮ Robust Model-Checking of Timed Automata via Pumping in Channel Machines ⋮ Unnamed Item ⋮ Model Checking Real-Time Systems ⋮ Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions ⋮ Priority-free conditionally-preemptive scheduling of modular sporadic real-time systems ⋮ Model Checking of Biological Systems ⋮ How to stop time stopping ⋮ Predicate diagrams for the verification of real-time systems ⋮ Model checking of time Petri nets using the state class timed automaton ⋮ Specification and analysis of the AER/NCA active network protocol suite in real-time Maude ⋮ Rewriting modulo SMT and open system analysis ⋮ Hybridization methods for the analysis of nonlinear systems ⋮ SetExp: a method of transformation of timed automata into finite state automata ⋮ Semantics and pragmatics of real-time maude ⋮ Automated repair for timed systems ⋮ The power of reachability testing for timed automata ⋮ Generalized discrete timed automata: Decidable approximations for safety verification. ⋮ Model-checking timed automata with deadlines with Uppaal ⋮ Equivalence checking 40 years after: a review of bisimulation tools ⋮ Scenario-based verification of real-time systems using UPPAAL ⋮ Unnamed Item ⋮ Superposition as a decision procedure for timed automata ⋮ Reachability analysis for timed automata using max-plus algebra ⋮ Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions ⋮ Reachability relations of timed pushdown automata ⋮ Efficient verification of distributed real-time systems with broadcasting behaviors ⋮ Robust reachability in timed automata and games: a game-based approach ⋮ Timed Basic Parallel Processes ⋮ Progress-preserving Refinements of CTA ⋮ When are timed automata weakly timed bisimilar to time Petri nets? ⋮ Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp> ⋮ An approximation algorithm for box abstraction of transition systems on real state spaces ⋮ Constructing invariants for hybrid systems ⋮ Unnamed Item ⋮ The Unmet Challenge of Timed Systems ⋮ A menagerie of timed automata ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ A control synthesis approach for time discrete event systems ⋮ Reachability results for timed automata with unbounded data structures ⋮ A brief history of process algebra ⋮ Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format ⋮ Implementation and analysis of real-time communication protocol compositions ⋮ Effective Representation of RT-LOTOS Terms by Finite Time Petri Nets ⋮ Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude ⋮ M-nets: a survey ⋮ Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment ⋮ An Introduction to Timed Automata ⋮ Wireless ventilation control for large‐scale systems: The mining industrial case ⋮ Formalized Timed Automata ⋮ Timed verification of the generic architecture of a memory circuit using parametric timed automata ⋮ A Compositional Translation of Timed Automata with Deadlines to Uppaal Timed Automata ⋮ Hybrid systems: From verification to falsification by combining motion planning and discrete search ⋮ Parking Can Get You There Faster ⋮ Verification of Linear Duration Invariants by Model Checking CTL Properties ⋮ A partial order semantics approach to the clock explosion problem of timed automata ⋮ A theory of stochastic systems. I: Stochastic automata ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Symbolic model checking of timed guarded commands using difference decision diagrams ⋮ Abstraction and Completeness for Real-Time Maude ⋮ Specification of real-time and hybrid systems in rewriting logic ⋮ Checking timed Büchi automata emptiness efficiently
This page was built for publication: Kronos: A verification tool for real-time systems
