• HyTech

  • Referenced in 333 articles [sw04125]
  • temporal requirement. Hybrid systems are specified as collections of automata with discrete and continuous components ... temporal requirements are verified by symbolic model checking. If the verification fails, then HyTech generates...
  • HYSDEL

  • Referenced in 39 articles [sw05200]
  • modeling a class of hybrid systems described by interconnections of linear dynamic systems, automata...
  • COSMOS

  • Referenced in 6 articles [sw13329]
  • COSMOS: a statistical model checker for the hybrid automata stochastic logic. This tool paper introduces ... Cosmos, a statistical model checker for the Hybrid Automata Stochastic Logic (HASL). HASL employs Linear ... Hybrid Automata (LHA), a gen eralization of Deterministic Timed Automata (DTA), to describe relevant execution ... Stochastic Process (DESP), a class of stochastic models which includes, but is not limited...
  • CalCS

  • Referenced in 8 articles [sw13098]
  • including formulas generated from bounded model checking of hybrid automata and static analysis of floating...
  • R-Charon

  • Referenced in 4 articles [sw19756]
  • reconfiguration to the existing distributed hybrid system modeling language Charon. The target application domain ... Charon is the first formal, hybrid automata based modeling language which also addresses dynamic reconfiguration...
  • HARE

  • Referenced in 4 articles [sw10938]
  • Hybrid automata-based CEGAR for rectangular hybrid systems. In this paper we present a framework ... abstraction-refinement (CEGAR) for systems modelled as rectangular hybrid automata. The main difference, between ... rectangular hybrid automata and complete for the subclass of initialized rectangular automata. We have implemented ... calls to HyTech to analyze the abstract models and validate the counterexamples. Our experiments demonstrate...
  • BACH

  • Referenced in 4 articles [sw11906]
  • linear hybrid automata. Hybrid automata are well studied formal models for hybrid systems with both ... state changes. However, the analysis of hybrid automata is quite difficult. Even for the simple...
  • HASL

  • Referenced in 6 articles [sw13330]
  • statistical verification of stochastic models. We introduce the Hybrid Automata Stochastic Logic (HASL...
  • HYST

  • Referenced in 8 articles [sw20137]
  • HYST approach provides a single place for model modification, generating modified input sources ... hybrid automata) to the input formats of several tools. Additionally, we illustrate a general model...
  • CellExcite

  • Referenced in 1 article [sw35366]
  • simulation, and customize the diffusion model. CellExcite adopts Hybrid Automata (HA) as the computational model...
  • SReach

  • Referenced in 5 articles [sw20158]
  • models of stochastic hybrid systems. The first one is (nonlinear) hybrid automata with parametric uncertainty ... second one is probabilistic hybrid automata with additional randomness for both transition probabilities and variable ... Standard approaches to reachability problems for linear hybrid systems require numerical solutions for large optimization ... applicability by discussing three representative biological models and additional benchmarks for nonlinear hybrid systems with...
  • LySHA

  • Referenced in 4 articles [sw20150]
  • loops of the hybrid automaton. The algorithm is complete for automata that are symmetric with ... integrated with a Simulink/Stateflow frontend for modeling hybrid systems. The experimental results demonstrate the effectiveness ... methodology in verifying inevitability of hybrid automata with up to five continuous dimensions and forty...
  • FORTS

  • Referenced in 1 article [sw15029]
  • FORTS). FORTS is a model checker on Linear Hybrid Automata (LHA) that I write ... FORTS compose a parser to read LHA models in script inputs and an engine...
  • HyDI

  • Referenced in 3 articles [sw11912]
  • validation techniques. Hybrid automata are a clean and consolidated formal language for modeling embedded systems ... model the continuous dynamics. In this paper, we propose a new language, HYDI, for modeling ... Hybrid systems with Discrete Interaction. The purpose of the language is to apply state...
  • HyLink

  • Referenced in 0 articles [sw20141]
  • restricted class of SLSF models to hybrid automata for verification...
  • StonyCam

  • Referenced in 3 articles [sw02004]
  • modeling, analyzing and regulating the behavior of cardiac tissues. Based on the theory of hybrid ... automata, we aim at providing suitable tools to be used in devising strategies...
  • CANv2

  • Referenced in 2 articles [sw39764]
  • CANv2: a hybrid CA model by micro- and macro-dynamics examples. Cellular Automata ... taken into account justifying the introduction of hybrid components between single cellular automata...
  • HyCreate

  • Referenced in 2 articles [sw20138]
  • hybrid automata through the interface, using the standard hybrid automaton model. The mode differential equations...
  • HyComp

  • Referenced in 4 articles [sw20163]
  • hybrid systems. HyComp is a model checker for hybrid systems based on Satisfiability Modulo Theories ... HyComp takes as input networks of hybrid automata specified using the HyDI symbolic language. HyComp...
  • SL2SX

  • Referenced in 1 article [sw20160]
  • application of formal verification techniques to Simulink models could help to overcome this limitation ... underlying formalism hybrid automata, which are semantically and structurally different from Simulink models. To address...