• Kronos

  • Referenced in 243 articles [sw01270]
  • real-time systems are modeled by timed automata and the correctness requirements are expressed...
  • Esterel

  • Referenced in 142 articles [sw20012]
  • programming reactive systems, including real-time systems and control automata. The Esterel v5 compiler...
  • VerICS

  • Referenced in 29 articles [sw02011]
  • original tool for automated verification of Timed Automata and protocols written in a subset ... original intermediate language (IL), or Timed Automata in the Kronos-like format can be used ... specification can be translated to timed automata, which are passed to other Verics components ... translating the reachability problem for Timed Automata to the satisfiability problem of propositional formulas...
  • IF-2.0

  • Referenced in 44 articles [sw03303]
  • intermediate representation language based on extended timed automata. In particular, this representation allowed...
  • TREX

  • Referenced in 43 articles [sw01388]
  • tool for automatic analysis of automata-based models equipped with variables belonging to different infinite/finite ... present time, parametric (continuous-time) timed automata, extended with integer counters and finite-domain variables...
  • LTL2BA

  • Referenced in 84 articles [sw10956]
  • algorithm to generate Büchi automata from Linear Time Logic (LTL) formulae. This algorithm generates...
  • IMITATOR

  • Referenced in 20 articles [sw00439]
  • synthesizing constraints on timing bounds of timed automata We present here Imitator, a tool ... parameters) in the framework of timed automata. Unlike classical synthesis methods, we take advantage ... values of the reference valuation, and optimizing timing bounds of the system. We have successfully...
  • TorX

  • Referenced in 17 articles [sw07155]
  • means of non-deterministic safety timed automata. This paper describes the basic algorithms for ioco ... necessary modifications to standard safety timed automata to make them usable as an input formalism ... test-derivation algorithm from timed automata, and the concrete algorithms implemented in TorX for timed...
  • UPPAAL TIGA

  • Referenced in 36 articles [sw12913]
  • algorithm for solving games based on timed game automata with respect to reachability and safety...
  • Romeo

  • Referenced in 24 articles [sw00812]
  • performs translations from TPNs to Timed Automata (TAs) that preserve the behavioural semantics (timed bisimilarity...
  • Rabbit

  • Referenced in 23 articles [sw01317]
  • time systems. The modeling language are timed automata extended with concepts for modular modeling...
  • TAXYS

  • Referenced in 21 articles [sw01389]
  • formal model of timed automata. The choice of this model allows the use of results ... code and on the other hand a timed model of the application. This model...
  • Synthia

  • Referenced in 7 articles [sw12933]
  • Synthia: Verification and synthesis for timed automata. Synthia is the first certifying model checker ... time systems modeled as networks of timed automata. The key innovation of Synthia ... unimplemented parts. In the analysis of timed automata, the main technical challenge is to efficiently...
  • Verics

  • Referenced in 5 articles [sw09464]
  • erics: A Tool for Verifying Timed Automata and Estelle Specifications. The paper presents ... tool for automated verification of Timed Automata as well as protocols written in the specification ... automatic translation from Estelle specifications to timed automata, and two complementary methods of reachability analysis...
  • TAPAAL

  • Referenced in 8 articles [sw00947]
  • Petri net models into networks of timed automata and uses the UPPAAL engine...
  • Shrinktech

  • Referenced in 4 articles [sw11890]
  • tool for the robustness analysis of timed automata. We present a tool for the robustness ... analysis of timed automata that can check whether a given time-abstract behaviour...
  • Tempo

  • Referenced in 5 articles [sw11778]
  • event-recording automata, a subclass of timed automata. This algorithm is based on a forward ... develop a real-time logic for specifying properties of event-recording automata in a suitable...
  • opaal

  • Referenced in 6 articles [sw13332]
  • verification of models using lattice automata. Lattice automata allow the users to incorporate abstractions ... supports a subset of the UPPAAL timed automata language extended with lattice features. We report...
  • REDLIB

  • Referenced in 5 articles [sw21175]
  • full TCTL model-checking of dense-time automata with multiple fairness assumptions. REDLIB uses ... efficient representation and manipulation of dense-time statespaces. Users can use the procedures in REDLIB...
  • LARVA

  • Referenced in 5 articles [sw21408]
  • number of notations, including timed-automata enriched with stopwatches, Lustre, and a subset of duration ... transactions. LARVA also performs analysis of real-time properties, to calculate, if possible, an upper...