Kronos: A verification tool for real-time systems
From MaRDI portal
Publication:1856194
DOI10.1007/s100090050009zbMath1060.68606MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Unnamed Item, Verification of Linear Duration Invariants by Model Checking CTL Properties, Kronos, Checking timed Büchi automata emptiness efficiently, How to stop time stopping, 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, Hybridization methods for the analysis of nonlinear systems, Semantics and pragmatics of real-time maude, When are timed automata weakly timed bisimilar to time Petri nets?, Implementation and analysis of real-time communication protocol compositions, Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude, M-nets: a survey, The power of reachability testing for timed automata, Generalized discrete timed automata: Decidable approximations for safety verification., Specification of real-time and hybrid systems in rewriting logic, A brief history of process algebra, 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, Presburger liveness verification of discrete timed automata., Updatable timed automata, Scheduling with timed automata, Constructing invariants for hybrid systems, A control synthesis approach for time discrete event systems, A partial order semantics approach to the clock explosion problem of timed automata, A theory of stochastic systems. I: Stochastic automata, Predicate diagrams for the verification of real-time systems, Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions, Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format, Effective Representation of RT-LOTOS Terms by Finite Time Petri Nets
