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:

Tool Description Link
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
Ptolemy II Ptolemy II is an open-source software framework supporting experimentation with actor-oriented design. open
LUSTRE LUSTRE is a data flow synchronous language, designed for programming reactive system.  open
MODEST The Modest toolset supports the modelling and analysis of hybrid, real-time, distributed and stochastic systems. open
HyLink HyLink is a tool which links Simulink/Stateflow models(SLSF) to the world of hybrid automaton. open
CHARON CHARON is a language for modular specification of interacting hybrid systems based on the notions of agent and mode. open
IOA IOA is a formal language for describing computational processes that are modeled using I/O automata. open
Möbius Möbius™ is a software tool for modeling the behavior of complex systems. open
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


Verification of Hybrid Systems:

Tool Description Link
Evrostos Evrostos is the first tool for model checking formulas in Robust Linear Temporal Logic (rLTL). open
JuliaReach JuliaReach is a toolbox for set-based reachability analysis of dynamical systems. open
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
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
AVERIST AVERIST implements an algorithmic approach for the stability analysis of polyhedral switched systems. open
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
HyLAA Hylaa (HYbrid Linear Automata Analyzer) is a verification tool for system models with linear ODEs, time-varying inputs, and possibly hybrid dynamics. open
STORM Storm is a tool for the analysis of systems involving random or probabilistic phenomena. open
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
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
C2E2 C2E2 is a tool for verifying hybrid automata. C2E2 can automatically check bounded time invariant properties of nonlinear hybrid automata. open
dReach dReach is a bounded reachability analysis tool for nonlinear hybrid systems. open
Flow* Flow*: an analyzer for non-linear hybrid systems. It performs Taylor model-based flowpipe construction for non-linear (polynomial) hybrid systems. open
HyComp HyComp is a model checker for hybrid systems based on satisfiability modulo theories (SMT). open
ProbReach ProbReach is collection of tools for calculating probability of bounded reachability in hybrid systems with parametric uncertainties. open
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
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
VeriSiMPL This toolbox is used to generate finite abstractions of autonomous Max-Plus-Linear (MPL) systems over R^n. open
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
OCRA OCRA is a command-line tool for the verification of logic-based contract refinement for embedded systems. open
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
BigMC BigMC (Bigraphical Model Checker) is a model-checker designed to operate on Bigraphical Reactive Systems (BRS). open
CORA The COntinuous Reachability Analyzer (CORA) is a collection of MATLAB classes for the formal verification of cyber-physical systems using reachability analysis. open
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
Passel Passel is a software tool for analyzing networked hybrid models with arbitrarily many components. open
PyPPL The Parma Polyhedra Library (PPL) provides numerical abstractions especially targeted at applications in the field of analysis and verification of complex systems. open
opaal opaal is a distributed/parallel (discrete time) model checker for networks of timed automata implemented in Python using MPI. open
SpaceEx The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification.  open
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
JTLV JTLV is a tool aimed to facilitate and provide a unified framework to the development of formal verification algorithms. open
PASS PASS is an analysis tool for infinite-state probabilistic models. It is based on predicate abstraction and automatic abstraction refinement.  open
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
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
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
KeYmaera 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
MLSolver A tool for solving the satisfiability and validity problems for modal fixpoint logics. open
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
SAAtRe AAtRe is an abstraction refinement model checker for timed automata based on extended SAT-solving techniques.  open
MATISSE MATISSE is a free MATLAB toolbox for safety verification and reachable set computation of large dimensional, constrained linear systems. open
PHAVer PHAVer is a new tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives.  open
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
PRISM 2 PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.  open
Polychrony Polychrony is an integrated development environment and technology demonstrator. open
d/dt d/dt is a tool for reachability analysis of continuous and hybrid systems with linear differential inclusions. open
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
NBAC NBAC analyses synchronous and deterministic reactive systems containing combination of Boolean and numerical variables and continuously interacting with an external environment.  open
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
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


Controller Synthesis for Hybrid Systems:

Tool Description Link
pFaces/GBFP pFaces/GBFP is a kernel inside the acceleration ecosystem pFaces. It can construct symbolic models of dynamial systems and synthesise their controllers. open
StocHy StocHy simplifies both the modelling and design of stochastic hybrid systems (SHS) and their analysis.  open
BoSy BoSy is a synthesis tool based on a various bounded synthesis encodings. open
ROCS ROCS is an algorithmic control synthesis tool for nonlinear dynamical systems. open
SafetySynth SafetySynth is a tool for synthesizing controllers from safety benchmarks given in the SyntComp AIGER format. open
SENSE SENSE is a tool for the automatic controller synthesis of complex plants in the networked control systems (NCS) based on symbolic models. open
DSSynth DSSynth synthesizes sound digital controllers for physical plants that are represented as linear time-invariant systems with single input and output. open
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
Sapo Sapo is a tool for the formal analysis of polynomial dynamical systems. Its main features are reachability computation and parameter synthesis. open
SCOTS SCOTS is a tool for the automatic controller synthesis of nonlinear control systems based on symbolic models. open
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
BluSTL BluSTL (pronounced "blue steel") is a MATLAB toolkit for automatically generating hybrid controllers from specifications written in Signal Temporal Logic. open
Demiurge Demiurge is a tool to synthesize a correct-by-construction implementation of a reactive system from a declarative safety specification.  open
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
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
AbsSynthe Swiss AbsSynthe - is the native version of the AbsSynthe tool, used to synthesize controllers from succinct safety specifications. open
CoSyMA CoSyMA is a tool for automatic controller synthesis for incrementally stable switched systems based on multi-scale discrete abstractions.  open
LtlOpt LtlOpt is a Matlab tool for the optimal control of high-dimensional, nonlinear robotic systems with linear temporal logic (LTL) specifications. open
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
Pessoa 2.0 Pessoa is a tool for the synthesis of correct-by-design embedded control software. open
TuLiP TuLiP is a tool for automatic synthesis of correct-by-construction embedded control software. open
ARCS ARCS is a toolbox for abstraction-refinement-based incremental synthesis of correct-by-construction switching protocols. open
Mascot Mascot is a tool for synthesizing controllers for continuous non-linear dynamical systems. open
Synthia Synthia is a tool for the verification and synthesis of open real-time systems modeled as timed automata. open
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
Quasy Quasy is a tool for synthesis of reactive systems which takes qualitative and quantitative specifications in GOAL format. open
RATSY A tool for Requirements Analysis with Synthesis open
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
GIST Gist is a tool for solving probabilistic games with ω-regular objectives qualitatively.  open
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
ALPAGA Alpaga is a software tool computing strategies for imperfect information parity games, using antichains during the computations to gain efficiency. open


Other tools:

Tool Description Link
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
COTONN COTONN is a a tool for converting symbolic controllers (from SCOTS) into neural network representation. open
SCOTS2FPGA SCOTS2FPGA provides space efficient implementations of symbolic controllers on FPGAs. open
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
SL2SX SL2SX is a tool that translates Simulink models (saved in XML format) into SpaceEx models (respecting the SX format). open