Tools for Hybrid Systems

In the lists below, we summarize the current actively-maintained tools for the analysis
and synthesis of hybrid systems. The lists are compiled by Prof. Dr. Manuel Mazo and
Mr. Mahmoud Khaled

Modeling and Identification (Languages and Tools):

 Tool  Description  Link  Last Maitained
SARXSAT SARXSAT is a tool for the identification of Switched and Piece-wise ARX models employing sparsification via l_0 minimization and SAT solvers.  open 10.2019
Ptolemy II Ptolemy II is an open-source software framework supporting experimentation with actor-oriented design. open 06.2018
LUSTRE LUSTRE is a data flow synchronous language, designed for programming reactive system. Tools like SCADE use LUSTRE. open N/A
MODEST The Modest toolset supports the modelling and analysis of hybrid, real-time, distributed and stochastic systems. open 09.2019
HyLink HyLink is a tool which links Simulink/Stateflow models(SLSF) to the world of hybrid automaton. open 08.2012
CHARON CHARON is a language for modular specification of interacting hybrid systems based on the notions of agent and mode. open N/A
IOA IOA is a formal language for describing computational processes that are modeled using I/O automata. open 08.2003
Möbius Möbius™ is a software tool for modeling the behavior of complex systems. open 12.2018
SIGNAL SIGNAL is a programming language based on synchronized data-flow (flows + synchronization): a process is a set of equations on elementary flows describing both data and control. open N/A


Verification of Hybrid Systems:

 Tool  Description  Link  Last Maitained
Evrostos Evrostos is the first tool for model checking formulas in Robust Linear Temporal Logic (rLTL). open 12.2020
JuliaReach JuliaReach is a toolbox for set-based reachability analysis of dynamical systems. open 12.2020
PIRK PIRK is a tool to efficiently compute reachable sets for general nonlinear systems of extremely high dimensions. It introduces three parallel algorithms for computing interval approximations of forward reachable sets. open 02.2020
SReachTools SReachTools is an open-source MATLAB toolbox for performing stochastic reachability of linear, potentially time-varying, discrete-time systems that are perturbed by a stochastic disturbance.  open 05.2020
TIRA TIRA is a Matlab library gathering several methods for the computation of interval over-approximations of the reachable sets for both continuous- and discrete-time nonlinear systems. open 12.2019
AVERIST AVERIST implements an algorithmic approach for the stability analysis of polyhedral switched systems. open 03.2015
DSValidator DSValidator is an automated counterexample reproducibility tool based on MATLAB, with the goal of reproducing counterexamples that refute specific properties related to digital systems. open 07.2017
HyLAA Hylaa (HYbrid Linear Automata Analyzer) is a verification tool for system models with linear ODEs, time-varying inputs, and possibly hybrid dynamics. open 10.2019
STORM Storm is a tool for the analysis of systems involving random or probabilistic phenomena. open 06.2020
xSAP xSAP is a tool for safety assessment of synchronous finite-state and infinite-state systems. It is based on symbolic model checking techniques. open 03.2016
Axelerator Axelerator is a tool for reachability analysis of open guarded linear time Invariant systems through the use of abstract acceleration. The tool allows the evaluation of reach tubes for both finite and infinite time horizons. open 06.2019
C2E2 C2E2 is a tool for verifying hybrid automata. C2E2 can automatically check bounded time invariant properties of nonlinear hybrid automata. open 11.2018
dReach dReach is a bounded reachability analysis tool for nonlinear hybrid systems. open 12.2020
Flow* Flow*: an analyzer for non-linear hybrid systems. It performs Taylor model-based flowpipe construction for non-linear (polynomial) hybrid systems. open 03.2017
HyComp HyComp is a model checker for hybrid systems based on satisfiability modulo theories (SMT). open 10.2014
ProbReach ProbReach is collection of tools for calculating probability of bounded reachability in hybrid systems with parametric uncertainties. open 11.2019
CoVerTS CoVerTS is a tool for the verification of state properties for timed systems. it served as a proof of concept for "Compositional Invariant Generation for Timed Systems". open 12.2014
JSR JSR is a toolbox for computing the Joint Spectral Radius of a set of matrices, i.e., the maximal asymptotic growth rate of products of matrices taken in that set. open 03.2016
VeriSiMPL This toolbox is used to generate finite abstractions of autonomous Max-Plus-Linear (MPL) systems over R^n. open 12.2016
HyCreate HyCreate is a software tool for defining hybrid automata and computing over-approximations of reachable sets for systems with nonlinear, nondeterministic dynamics with a small number of dimensions. open 03.2018
OCRA OCRA is a command-line tool for the verification of logic-based contract refinement for embedded systems. open 07.2020
Stabhyli Stabhyli is a tool that automatically proves stability (global asymptotic stability) of non-linear hybrid systems. The tool was created in the context of AVACS H4. open 11.2015
BigMC BigMC (Bigraphical Model Checker) is a model-checker designed to operate on Bigraphical Reactive Systems (BRS). open 08.2012
CORA The COntinuous Reachability Analyzer (CORA) is a collection of MATLAB classes for the formal verification of cyber-physical systems using reachability analysis. open 11.2018
HYMITATOR HYMITATOR is a tool dedicated to the synthesis of parameters for hybrid automata (HA). It is a fork of IMITATOR, the tool for parameter synthesis in timed automata. open 04.2012
Passel Passel is a software tool for analyzing networked hybrid models with arbitrarily many components. Passel is now integrated as a module in HyST (see details below). open 04.2014
PyPPL The Parma Polyhedra Library (PPL) provides numerical abstractions especially targeted at applications in the field of analysis and verification of complex systems. open 02.2016
opaal opaal is a distributed/parallel (discrete time) model checker for networks of timed automata implemented in Python using MPI. open 11.2016
SpaceEx The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification.  open 02.2015
CARTS CARTS (Compositional Analysis of Real-Time Systems) is developed as a platform-independent tool that automatically generates resource interfaces needed for the compositional analysis of real-time systems. open 06.2018
JTLV JTLV is a tool aimed to facilitate and provide a unified framework to the development of formal verification algorithms. open 03.2008
PASS PASS is an analysis tool for infinite-state probabilistic models. It is based on predicate abstraction and automatic abstraction refinement.  open 07.2012
INFAMY INFAMY is a tool with the purpose of model checking CSL formulae on infinite state Markov chains in continuous time, specified in a variant of the PRISMlanguage. open 12.2009
Roméo Roméo is a software studio for Time Petri Net analysis, developed in the Real-Time Systems Team at IRCCyN . It performs analysis on T-Time Petri nets and on one of their extension to scheduling. open 11.2020
BACH BACH stands for Bounded reAcheability CHecker, it is a bounded model checker for Linear Hybrid Systems. BACH was designed and implemented by Software Engineering Group, Nanjing University. open 05.2017
KeYmaera X
KeYmaera is A hybrid theorem prover for hybrid systems. KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. open 12.2020
MLSolver A tool for solving the satisfiability and validity problems for modal fixpoint logics. open 12.2016
HSolver HSolver is a program for verification of hybrid systems based on the constraint solver RSOLVER. Unlike other packages its correctness does not depend on floating point rounding errors. It can handle non-linear ordinary differential equations, but is not optimized for simpler continuous dynamics. open 11.2007
SAAtRe AAtRe is an abstraction refinement model checker for timed automata based on extended SAT-solving techniques.  open 10.2012
MATISSE MATISSE is a free MATLAB toolbox for safety verification and reachable set computation of large dimensional, constrained linear systems. open 07.2005
PHAVer PHAVer is a new tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives.  open 02.2007
Hybrid Toolbox for MATLAB The Hybrid Toolbox is a MATLAB/Simulink toolbox for modeling, simulating, and verifying hybrid dynamical systems, for designing and simulating model predictive controllers for hybrid systems subject to constraints, and for generating linear and hybrid MPC control laws in piecewise affine form that can be directly embedded as C-code in real-time applications. open 11.2020
PRISM 2 PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.  open 04.2020
Polychrony Polychrony is an integrated development environment and technology demonstrator. open 05.2010
Sigali Sigali is a model-checking tool-based which manipulates ILTS: Implicit Labeled Transition Systems (which can be seen as an equational representation of an automaton) as intermediate models for discrete event systems. open 06.2007
NBAC NBAC analyses synchronous and deterministic reactive systems containing combination of Boolean and numerical variables and continuously interacting with an external environment.  open 02.2011
HyTech HyTech is an automatic tool for the analysis of embedded systems. HyTech computes the condition under which a linear hybrid system satisfies a temporal requirement. open 06.2002
UPPAAL Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.). open 11.2019


Controller Synthesis for Hybrid Systems:

 Tool  Description  Link  Last Maitained
OmegaThreads OmegaThreads is a tool for parallel automated controller synthesis for dynamical systems to satisfy ω-regular specifications given as LTL formulae. open 12.2020
pFaces pFaces is an the acceleration ecosystem for formal methods.  open 10.2020
StocHy StocHy simplifies both the modelling and design of stochastic hybrid systems (SHS) and their analysis.  open 12.2019
BoSy BoSy is a synthesis tool based on a various bounded synthesis encodings. open 12.2017
ROCS ROCS is an algorithmic control synthesis tool for nonlinear dynamical systems. open 12.2020
SafetySynth SafetySynth is a tool for synthesizing controllers from safety benchmarks given in the SyntComp AIGER format. open 12.2016
AMYTISS AMYTISS builds finite Markov decision processes (MDPs) as finite abstractions from stochastic discrete-time systems and synthesizes controllers for them satisfying bounded-time safety specifications and reach-avoid specifications. open 06.2020
SENSE SENSE is a tool for the automatic controller synthesis of complex plants in the networked control systems (NCS) based on symbolic models. open 12.2018
DSSynth DSSynth synthesizes sound digital controllers for physical plants that are represented as linear time-invariant systems with single input and output. open 12.2019
QUEST QUEST is a tool for automated controller synthesis for incrementally input-to-state stable nonlinear control systems with respect to safety and reachability specifications. open 12.2017
Sapo Sapo is a tool for the formal analysis of polynomial dynamical systems. Its main features are reachability computation and parameter synthesis. open 12.2016
SCOTS SCOTS is a tool for the automatic controller synthesis of nonlinear control systems based on symbolic models. A ready/easy to install version is also available here. open 12.2019
slugs Slugs is a stand-alone reactive synthesis tool for generalized reactivity(1) synthesis. It uses binary decision diagrams (BDDs) as the primary data structure for efficient symbolic reasoning. open 01.2020
BluSTL BluSTL (pronounced "blue steel") is a MATLAB toolkit for automatically generating hybrid controllers from specifications written in Signal Temporal Logic. open 12.2014
Demiurge Demiurge is a tool to synthesize a correct-by-construction implementation of a reactive system from a declarative safety specification.  open 12.2015
FAUST 2 FAUST2 is a software tool that generates abstractions of (possibly non-deterministic) discrete-time Markov processes (dtMP) defined over uncountable (continuous) state spaces. open 02.2014
reasyns Reasyns generates a library of atomic controllers for nonlinear systems satisfying a high-level controller (a finite state machine) synthesized from a reactive mission specification. open 12.2016
AbsSynthe Swiss AbsSynthe - is the native version of the AbsSynthe tool, used to synthesize controllers from succinct safety specifications. open 03.2020
CoSyMA CoSyMA is a tool for automatic controller synthesis for incrementally stable switched systems based on multi-scale discrete abstractions.  open 11.2017
LtlOpt LtlOpt is a Matlab tool for the optimal control of high-dimensional, nonlinear robotic systems with linear temporal logic (LTL) specifications. open 08.2014
gr1c gr1c is a collection of tools for GR(1) synthesis and related activities. Its core functionality is checking realizability of and synthesizing strategies for GR(1) specifications, though it does much more. open 02.2020
Pessoa 2.0 Pessoa is a tool for the synthesis of correct-by-design embedded control software. open 06.2011
TuLiP TuLiP is a tool for automatic synthesis of correct-by-construction embedded control software. open 11.2016
ARCS ARCS is a toolbox for abstraction-refinement-based incremental synthesis of correct-by-construction switching protocols. open 12.2018
Mascot Mascot is a tool for synthesizing controllers for continuous non-linear dynamical systems. open 12.2018
Synthia Synthia is a tool for the verification and synthesis of open real-time systems modeled as timed automata. open 12.2011
TALIRO-TOOLS TALIRO (TemporAl LogIc RObustness) tools is a suit of tools for the analysis of continuous and hybrid dynamical systems using linear time temporal logics. open 10.2019
Quasy Quasy is a tool for synthesis of reactive systems which takes qualitative and quantitative specifications in GOAL format. open 07.2011
Unbeast Unbeast is a tool capable of handling full linear-time temporal logic (LTL). It is designed for specifications comprising a set of assumptions and a set of guarantees. open 11.2012
LTLMoP The LTLMoP (Linear Temporal Logic MissiOn Planning) toolkit is a collection of Python applications for designing, testing, and implementing hybrid controllers generated automatically from task specifications written in Structured English or Temporal Logic. open 12.2015
ALPAGA Alpaga is a software tool computing strategies for imperfect information parity games, using antichains during the computations to gain efficiency. open 12.2009


Other tools:

 Tool  Description  Link  Last Maitained
BDD2Implement BDD2Implement is a tool to generate hardware/software implementations of BDD-based symbolic controllers. The implementations come in form of source-code (VHDL/Verilog for FPGAs and C/C++ for other systems). open 10.2020
COTONN COTONN is a a tool for converting symbolic controllers (from SCOTS) into neural network representation. open 12.2018
SCOTS2FPGA SCOTS2FPGA provides space efficient implementations of symbolic controllers on FPGAs. open 06.2019
HYST HYST is a HYbrid Source Transformer. HYST is a source-to-source translation tool, currently taking input in the SpaceEx model format, and translating to the formats of HyCreate, Flow*, or dReach.  open 04.2015
SL2SX SL2SX is a tool that translates Simulink models (saved in XML format) into SpaceEx models (respecting the SX format). open 12.2017