• LARVA

  • Referenced in 6 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...
  • GEZEL

  • Referenced in 6 articles [sw04151]
  • relate this domain to the timed-automata model and we have experimented with verification...
  • COSMOS

  • Referenced in 5 articles [sw13329]
  • eralization of Deterministic Timed Automata (DTA), to describe relevant execution paths of a Discrete Event...
  • 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...
  • Casaal

  • Referenced in 5 articles [sw10130]
  • approach and implementation for analysing weighted timed automata (WTA) with respect to the weighted metric ... WMTL ≤ , allowing for efficient SMC by run-time evaluation of a given formula. By necessity...
  • LiQuor

  • Referenced in 18 articles [sw04136]
  • omega-regular linear time properties by means of automata-based model checking algorithms...
  • PEPS

  • Referenced in 34 articles [sw03186]
  • Automata Networks(SAN) models. In its sequential version, the cost of the execution time becomesimpracticable...
  • mctau

  • Referenced in 2 articles [sw07213]
  • formal semantics in terms of stochastic timed automata, an overarching formalism of which several well ... paper, we focus on networks of timed automata as supported by Uppaal. We report ... subset of Modest models to Uppaal timed automata and enable connections to further tools...
  • McAiT

  • Referenced in 3 articles [sw09947]
  • McAiT is that it leverages timed automata to model both the timing behaviors...
  • Timed Automata

  • Referenced in 1 article [sw28568]
  • Timed automata are a widely used formalism for modeling real-time systems, which is employed ... subclass of diagonal-free timed automata, which is sufficient to model many interesting problems ... concepts and semantics of diagonal-free timed automata. Based on this, we prove two types...
  • DCVALID

  • Referenced in 14 articles [sw20416]
  • based on an automata theoretic decision procedure for Quantified Discrete-time Duration Calculus (QDDC ... efficient multi-terminal BDD based representation of automata and has implemented algorithms for operations...
  • Calife

  • Referenced in 1 article [sw28607]
  • several automata models (transition systems, timed automata, counter automata,...) and allows to define new models ... Kronos, CMC, Coq,...) and a unique timed-automata system modelled under the Calife System Editor...
  • HighSpec

  • Referenced in 1 article [sw09750]
  • combination of Object-Z (OZ) and Timed Automata (TA). Building on the strength of Object ... specifying data structures and Timed Automata’s in modelling dynamic and real-time behaviors, OZTA...
  • CATS

  • Referenced in 1 article [sw17954]
  • real-time systems modeled using timed automata and the real-time calculus. It is based...
  • TarTar

  • Referenced in 1 article [sw37080]
  • TarTar: a timed automata repair tool. We present TarTar, an automatic repair analysis tool that...
  • ZenoTool

  • Referenced in 1 article [sw10129]
  • tool that analyzes model specifications of timed automata systems created with UPPAAL for the occurrence ... Runs. Zeno Runs are paths in the timed transition system where infinite actions are executed...
  • Time4sys2imi

  • Referenced in 1 article [sw31184]
  • tool translating Time4sys models into parametric timed automata in the input language of IMITATOR. This ... only to check the schedulability of real-time systems, but also to infer some timing...
  • ltl2dstar

  • Referenced in 4 articles [sw21007]
  • converts formulas in Linear Time Logic to deterministic ω-automata, specifically Rabin (DRA) and Streett...
  • DYANA

  • Referenced in 1 article [sw36150]
  • also transformed into a Network of Timed Automata (NTA). After translation into...
  • Moby/DC

  • Referenced in 5 articles [sw01395]
  • real-time specifications. We define an operational subset of Duration Calculus, called phase automata, which ... real-time system descriptions that contain timing parameters. We introduce the tool MOBY/DC which implements ... model-checking algorithm for phase automata. The algorithm applies compositional model-checking techniques and handles...