Recent softwares
MOCHY
- MOCHY is the acronym for Models for Concurrent Hybrid Systems. This open source toolbox
allows for the modeling of hybrid systems, schedule and regulation algorithms
to optimize Key Performance Indicators. The tool is tailored for fast simulation of these regulated
models, to measure performance indicators. It is designed to be open ans allow you to use the simulation
engine with your own models. Sources and latest executable versions are available from
the GITLAB page of the project.
Contact : loic.helouet@inria.fr
SIMSTORS
- SIMSTORS is a software for the simulation of stochastic concurrent timed systems. The software
allows for fast simulation of specifications described using a variant of stochasitc Petri nets, and
guided by a controller. The implementation was performed during the Master internship of Karim Kecir
in the SUMO team.
Contact : loic.helouet@inria.fr
ReaX
- ReaX is a tool
developed by N. Berthier and
Hervvé Marchand that investigates the control of safety
properties for infinite reactive synchronous systems modeled by
arithmetic symbolic transition systems (e.g., programs comprising
Boolean, real or integer variables). By using abstract
interpretation techniques involving disjunctive polyhedral
over-approximations, we provide effective symbolic algorithms
allowing to solve the deadlock-free safety control problem. As for
SIGALI, this tool is connected with the BZR/Heptagon environment.
ReaX is distributed under the terms of the GNU General Public
License. It is implemented in Ocaml and is a fork of the ReaVer tool
originally implemented by
Peter Schrammel .
Others
TGV
-
is a tool for test generation of conformance test suites from specifications of
reactive systems. It is based on the IOLTS
model, a well defined theory of testing, and on-the-fly test generation
algorithms coming from verification technology. Originally, TGV allows test
generation focussed on well defined behaviors formalized by test purposes.
The main operations of TGV are (1) a synchronous product which identifies
sequences of the specification accepted by a test purpose , (2) abstraction
and determinization for the computation of next visible actions, (3)
selection of test cases by reachability and coreachability. TGV has been
developed in collaboration with Verimag Grenoble and uses libraries of the
CADP toolbox (VERIMAG and VASY). TGV can be seen as a library that can be
linked to different simulation tools through well defined APIs. An academic
version of TGV is distributed in the CADP toolbox and allows test generation
from Lotos specifications by a connection to its simulator API. The same API
is used for a connection with the UMLAUT validation framework of UML models.
This version has been transfered in the SDL ObjectGeode toolset as part of
the TestComposer tool. A new version of TGV is currently adapted to a new
API of the IF simulator (VERIMAG) allowing test generation from IF and UML
models (via a compilation from UML to IF). This new version extends the
previous one with new functionalities for coverage based test generation
combined with test purposes based test generation. TGV is protected by APP
(Agence de Protection des Programmes).
Contact : thierry.jeron@irisa.fr
SIGALI
-
Sigali is a model-checking tool that operates on ILTS (Implicit Labeled
Transition Systems, an equational representation of an automaton), an
intermediate model for discrete event systems. It offers functionalities for
verification of reactive systems and discrete controller synthesis. It is
developed jointly by the ESPRESSO
and Vertecs teams.
The techniques used consist in manipulating the system of equations instead
of the sets of solution, which avoids the enumeration of the state space.
Each set of states is uniquely characterized by a predicate and the
operations on sets can be equivalently performed on the associated
predicates. Therefore, a wide spectrum of properties, such as liveness,
invariance, reachability and attractivity can be checked. Algorithms for the
computation of predicates on states are also available. SIGALI is connected
with the Polychrony
environment (as well as the Matou
environment), thus allowing the modeling of reactive systems by means of
Signal Specification or Mode Automata and the visualization of the
synthesized controller by an interactive simulation of the controlled system.
SIGALI is protected by APP (Agence de Protection des Programmes).
Contact : herve.marchand@irisa.fr
STG
- STG (Symbolic Test Generation) is a prototype tool for the generation and execution of test cases
using symbolic techniques. It takes as input a specification and a test
purpose described as IOSTS, and generates a test case program also in the
form of IOSTS. Test generation in STG is based on a syntactic product of the
specification and test purpose IOSTS, an extraction of the subgraph
corresponding to the test purpose, elimination of internal actions,
determinization, and simplification. The simplification phase now relies on
NBAC, which approximates reachable and coreachable states using abstract
interpretation. It is used to eliminate unreachable states, and to
strengthen the guards of system inputs in order to eliminate some
Inconclusive verdicts. After a translation into C++ or Java, test cases can
be executed on an implementation in the corresponding language. Constraints
on system input parameters are solved on-the-fly during execution.
Contact : vlad.rusu@irisa.fr
SOFAT
- SOFAT is the acronym for Scenario Oracle and Formal Analysis Toolbox. As this name suggests it is
a formal analysis toolbox for scenarios. Scenarios are informal descriptions of behaviors of distributed
systems. SOFAT allows the edition and analysis of distributed systems specifications described using Message
Sequence Charts, a scenario language standardized by the ITU [Z.120]. The main functionalities proposed
by SOFAT are the textual edition of Message Sequence Charts, their graphical visualization, the analysis of
their formal properties, and their simulation. The analysis of the formal properties of a Message Sequence
Chart specification determines if a description is regular, local choice, or globally cooperative. Satisfaction of
these properties allow respectively for model-checking of logical formulae in temporal logic, implementation,
or comparison of specifications. All these applications are either undecidable problems or unfeasible if
the Message Sequence Chart description does not satisfy the corresponding property. The SOFAT toolbox
implements most of the theoretical results obtained on Message Sequence Charts this last decade. It is regularly
updated and re-distributed. The purpose of this software is twofold:
Provide a scenario based specification tool for developers of distributed applications
Serve as a platform for theoretical results on scenarios and partial orders
SOFAT provides several functionalities, that are: syntactical analysis of scenario descriptions, Formal analysis
of scenario properties, Interactive Simulation of scenarios when possible, and diagnosis.
Contact : loic.helouet@inria.fr
DAXML
- DAXML is an implementation of Distributed Active Documents, a formalism for data centric design of
Web Services proposed by Serge Abiteboul. This implementation is based on a REST framework, and can
run on a network of machines connected to internet and equipped with JAVA.
This implementation was realized during the post doc of B. Masson in 2011.
We maintain this prototype as a demonstrator for our Web Services activities, and will soon distribute the sources.
Contact : loic.helouet@inria.fr