Specification Languages

Our group has defined the  IF intermediate representation for distributed real-time systems based on extending communicating timed automata.  This representation is expressive enough to capture most of the functional primitives existing in standard languages such as SDL and UML (parallel execution, communication media, complex data, dynamic creation and destruction, parameterization, etc) as well as non-functional aspects related to timing, performance and scheduling.

IF ensure an intermediate representation between high-level standards and low-level tool input formalisms.  Moreover, it has an operational semantics relating functionality and timing.  In particular, the work on IF and its semantics has lead to a new standardization submission for the real-time semantics of the SDL language.

Model-checking and Static Analysis

The group has a long record in developing and implementing efficient state-space exploration algorithms.  Our results are implemented in the IF environment - an open validation platform based on the IF representation - and  in CADP - a toolbox devoted to the validation of Lotos programs - developed in collaboration with Inria/Vasy.

Efficient static analysis techniques for mitigating the state-explosion problem have been developed and applied to several industrial case studies.  These techniques have been developed with particular care to real-time distributed systems that combine asynchronous communication with real-time aspects.  They are completely integrated in the IF environment.  

Test Case Generation

In collaboration with Irisa/Pampa, a model-based algorithm for generating functional test-cases for black-box testing has been developed. The algorithm is implemented in the TGV tool.