Contributions to verification and design tools
Persiform tool for performance analysis (2005-2007)
In the context of the Persiform project, we have defined a tool chain allowing to derive
from functional requirements expressed in an appropriate UML profile a performance model analysable
by the commercial performance analysis tool Hyperformix workbench.
Any legal model of this UML profile is translated via a series of transformations to a subset of procedural
coloured Petrinets, defining the semantics, and then via a general format for queuing networks
into the input format of Hyperformix workbench. In addition the tool performs some graphical layout for
increasing the usability.
Impact of the tool:
Presently it is too early to measure the impact of this tool. Nevertheless, it should have some potential
as it addresses a real demand in industry, the tool has a realistic performance and can be easily adapted
due to the modularity of the transformation chain. It is planned to be adapted for usage in the context
of the development of embedded system (for Airbus) in the context of the OpenEmBeDD project.
A website will be available soon
IF toolbox (since 1998)
IF is a language for the structured representation of concurrent real-time systems and a set of tools allowing
the analysis and verification of requirements on such systems.
The tool evolved from the CADP toolset. Its development was motivated by the need for
a structured representation of systems, allowing the application of simplifications for avoiding state
explosion before its translation into a global (symbolic) transition relation.
In particular, IF has frontends allowing the verification and analysis of models
of real-time systems represented in SDL and UML.
See also the IF website for more exhaustive information and references.
Impact of the tool:
The IF toolset has been used in a large number of Research projects as a verification tool and as a (common)
intermediate format. The tool itself has been the object of several transfert activities.
- Invariant checker (1995-1999)
This tool has been developed mainly in Hassen Saidi-F˘s PhD thesis. It takes
as inputs the same kind of descriptions as Oscar, extended to the set of types and functions that can be
used in PVS.
It consists of a checker and an abstractor tool. The checker extends the BDD-based boolean
symbolic model-checking technique for invariants of the form Always(p) to unions of guarded commands describing
symbolic transition systems expressible in the PVS expression language. It is based on the backwards
computation of the greatest fix-point of the transition relation that is included in a state predicate. The
termination condition of this algorithm is submitted as a verification condition to the theorem prover PVS,
using as a semi-decision procedure a proof tactic combining boolean simplifications, rewriting.
See also the Invariant checker website
for a more detailed description of the tool and its architecture.
Impact of the tool: We have demonstrated the usefulness of the implemented method on several case
studies. In particular, we have used this tool to verify a Bounded Retransmission
Protocol (BRP) (see also here
for a more detailed description of the case study).
The method implemented by the abstractor of the Invariant-checker has been taken over in many
successor tools which use different representations of symbolic transition systems and differ in the heuristics
used for calculating approximations of the exact abstract transition relation.
The Invariant checker has been maintained for many years by Hassen Saidi at SRI. Its functionalities
have been implemented in the InVesT tool which then has been extended to the verification of
parameterized systems in the PAX tool. Today these tools are not maintained anymore.
- Abstractor and Oscar (1991-1998)
These tools have been developed in the context of the thesis of Claire Loiseaux.
Abstractor allows, given (1) a Boolean transition system in the form of a union of transition relations
Ri described by a set of guarded commands on boolean variables and (2) an abstraction relation given
in the form of a boolean expression relating abstract and concrete boolean variables, to automatically
calculate an abstract boolean transition system of the same form.
Oscar allows evaluating on such boolean transition systems properties expressed by the LTAC extensions
developed in the Delta 4 project. It applies symbolic model-checking techniques
based on pre-image computations. In particular, we have defined some efficient algorithms for specific
Impact of the tool: Using this prototype, we have verified a set of safety properties of non trivial
examples, in particular a token ring protocol and a non trivial toy service in the context of an automated
highway, managing overtaking manoeuvres.
Oscar has not been exploited in its original form for a long period, but it is the kernel of SMI, the
Symbolic model interface, an API for several BDD packages, and it is the basis on which the first symbolic
model-checkers of CADP.
This symbolic model-checker has however been relatively little used over a long
period, as for the case studies we were faced with, the enumerative model-checkers turned out to be more
- XESAR, version 3.1 (1988-1990)
Xesar was a reimplementation of the CESAR model-checker [QueilleSifakis82] meant as an industrial
strength tool. It allowed the verification of requirements expressed in the temporal logic LTAC semantically
equivalent to CTL, but developed independently using different notations and binary modalities
on Kripke structures generated from descriptions in a rendez-vous based version of Estelle. The initial
version of the tool is limited to Kripke structures with 64K states and generates a Kripke structure
allowing the evaluation of any state predicate definable on the initial Estelle programme.
The enhancement developed in the Delta 4 project, called version 3.1, improves
the efficiency considerably:
Impact of the tool: Using the enhanced Xesar tool together with an appropriate validation methodology,
we succeeded in verifying the service properties of several variants of a fault tolerant atomic broadcast
The functionalities of the Xesar tool have been later integrated in the Aldearan and Caesar
tools, later called CADP which is still widely used.
- we propose high-level patterns for the expression of properties to improve
the acceptance by the users.
- We implement a model generation algorithm for a fixed set of a priori
defined state predicates and we use on-the-fly evaluation for enhancing the performance of the tool in the