
Kronos
 Referenced in 259 articles
[sw01270]
 realtime systems are modeled by timed automata and the correctness requirements are expressed...

Esterel
 Referenced in 161 articles
[sw20012]
 programming reactive systems, including realtime systems and control automata. The Esterel v5 compiler...

VerICS
 Referenced in 31 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 Kronoslike 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...

IF2.0
 Referenced in 46 articles
[sw03303]
 intermediate representation language based on extended timed automata. In particular, this representation allowed...

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

TREX
 Referenced in 45 articles
[sw01388]
 tool for automatic analysis of automatabased models equipped with variables belonging to different infinite/finite ... present time, parametric (continuoustime) timed automata, extended with integer counters and finitedomain variables...

TorX
 Referenced in 19 articles
[sw07155]
 means of nondeterministic 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 ... testderivation algorithm from timed automata, and the concrete algorithms implemented in TorX for timed...

UPPAAL TIGA
 Referenced in 38 articles
[sw12913]
 algorithm for solving games based on timed game automata with respect to reachability and safety...

IMITATOR
 Referenced in 27 articles
[sw00439]
 formalism of networks of parametric timed automata, augmented with integer variables and stopwatches. It implemented...

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

Rabbit
 Referenced in 24 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...

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

UPPAAL CORA
 Referenced in 9 articles
[sw25660]
 AMETIST projects. Whereas UPPAAL uses timed automata as its modelling language, UPPAAL CORA uses linearly ... priced timed automata (LPTA). Given an LPTA model, UPPAAL CORA finds the optimal paths ... goal conditions. This can significantly reduce the time required for finding a good...

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 6 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...

TAME
 Referenced in 5 articles
[sw28703]
 specialpurpose theorem proving. TAME (Timed Automata Modeling Environment), an interface to the theorem proving ... automata: I/O automata, LynchVaandrager timed automata, and SCR automata. TAME provides templates for specifying...

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 timeabstract behaviour...

Tempo
 Referenced in 5 articles
[sw11778]
 eventrecording automata, a subclass of timed automata. This algorithm is based on a forward ... develop a realtime logic for specifying properties of eventrecording automata in a suitable...

LARVA
 Referenced in 6 articles
[sw21408]
 number of notations, including timedautomata enriched with stopwatches, Lustre, and a subset of duration ... transactions. LARVA also performs analysis of realtime properties, to calculate, if possible, an upper...