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 |