Accueil > Équipes > Tempo > Outils > Outils
Outils
Vitrine
- AMT 2.0 Analog Monitoring Tool [Open-source distribution,
beta,
active maintenance]
AMT 2.0 is a tool for offline monitoring and measuring temporal specifications over discrete and continuous behaviors.
- Kronos
Kronos is a tool for model-checking of timed automata against specifications expressed using the real-time temporal logic TCTL.
- NLTOOLBOX
This library provides an algorithmic infrastructure for reachability computation of non-linear dynamical systems.
- PHAVer
PHAVer is a tool for reachability analysis of continuous and hybrid systems based on Linear Hybrid Automata.
- SpaceEx State Space Explorer [Open-source distribution,
active maintenance]
The SpaceEx platform, a tool designed to facilitate the implementation of algorithms related to reachability and safety verification of continuous and hybrid systems.
Autre
- d/dt
d/dt is a prototype tool for reachability analysis of continuous and hybrid systems
- Montre A Tool for Monitoring Timed Regular Expressions [Open-source distribution,
beta,
Montre is a monitoring tool to search patterns specified by timed regular expressions over real-time behaviors. It uses timed regular expressions as a compact, natural, and highly-expressive pattern specification language for monitoring applications involving quantitative timing constraints. The tool essentially incorporates online and offline timed pattern matching algorithms so it is capable of finding all occurrences of a given pattern over both logged and streaming behaviors. (...)
- ParetoLib Multidimensional Pareto Boundary Learning Library for Python [Open-source distribution,
beta,
This library implements an algorithm for learning the boundary between an upward-closed set X1 and its downward-closed component X2 (i.e., X=X1+X2). Generally, the library supports spaces X of dimension N. The algorithm selects sampling points x=(x1,x2,...,xN) for which it submits membership queries ’is x in X1 ?’ to an external Oracle. Based on the Oracle answers and relying on monotonicity, the algorithm constructs an approximation of the boundary, called the Pareto front. The algorithm (...)
- StreamExplorer [Binary distribution,
pre-alpha,
no maintenance]
Dataflow multi-core scheduling using SMT solvers.
Archive
The tools below are prototypes or tools that are not active anymore.- OpenKronos
OpenKronos : is an on-the-fly verification tool for timed automata based on an integration of the DBM library of Kronos into CADP.
