Construction of validation tools and their integration

We have developed and extended several tools for abstraction and symbolic verification of extended automata. We consider that the work done this year on this topic is an important step toward our objectives. Further work will be done next year to enhance the capabilities of our tools.

We have also defined a common language (IF) which allows integration of the tools in an SDL environment through a connection to ObjectGeode of Telelogic. The new version of the language (IF-2.0) extend the previous one by several features, mainly the possibility of handling procedures, and dynamic creation and destruction of processes. Extensions of the language have been proposed and are under study in order to be able to describe parametrized networks of processes. In particular, we plan to include quantification in expressions (e.g. guards). This is necessary to write global conditions on networks such as there exists a process instance such that, or all the processes of index greater than $i$ are such that.

We shall continue the work of integrating the tools through designing interfaces to the IF environment. We expect to make substantial progress by the end of the second year.

We will also consider the integration of analysis packages and representation structures packages developed by different partners. For instance, NDDs developed by the group of Liège (Liège) will be used by the group of Edinburgh (UEdin) in model-checking tools for recursive procedures with integer parameters.