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 Vérimag 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 SDLObjectGéode 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).
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).
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.
