Recent softwares

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.

    More details

    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).

    More details

    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).

    More details

    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.

    More details

    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.

    More details

    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.

    More details

    Contact : loic.helouet@inria.fr