Susanne Graf

• CNRS Research professor (Directeur de Recherche)
• in the MOHYTOS Team

• 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 and a tool for validating specifications written in IF.
  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 some references.
  
  Impact of the tool: The IF toolset has been used in many research projects as a verification tool and as a (common) intermediate format. The tool itself has been the object of several transfer activities. Today, mainly the tool IFx-OMEGA, a validation frontend for IF for a rich subset of UML 2.2/SysML 1.1 is maintained by Iulian Ober at IRIT.
• Persiform tool for performance analysis (2005-2010)
  
  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.
• Invariant checker (1995-1999)
  
  This tool has been developed mainly in Hassen Saidi'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 property patterns.
  
  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 has been 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 efficient.
• 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:
  1. we propose high-level patterns for the expression of properties to improve the acceptance by the users.
  2. 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 debugging phase.
  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 protocol. The functionalities of the Xesar tool have been later integrated in the Aldearan and Caesar tools, later called CADP which is intensively used and further developed until today.