DATE: Distributed DiAgnosability and TEstability of Faulty Systems

We are facing a numeric world where interleaved embedded devices, such as mechatronic, electronic and software functions, increase considerably inside systems, making them more and more complex. In addition most of these systems are distributed, either by nature (networks, Web applications, etc.) or for privacy reasons (each subsystem model being hidden from other subsystems). They also interact with other subsystems and the environment (physical or human). And a lot are critical. The tasks of formally validating that these systems will operate properly, according to their specifications at design stage, during their functioning, and that any dysfunction due to the occurrence at any moment of some - hardware of software - fault (from a given list of anticipated faults) will be identified without ambiguity in finite time (in order to trigger recovery functions) are thus a major socio-economic concern and a real challenge. They are respectively addressed by testability and diagnosability methods. Both are model-based approaches (using a specification model, correct and faulty models of the system, an observation model, etc.) and rely on model checking techniques ensuring formally that some given properties are satisfied by a model. Though close in their objectives and methods, no unifying framework has been proposed up to now for testability and diagnosability. And attempts to adapt these two methods, traditionally developed for centralized systems, to decentralised or distributed ones are very recent and still preliminary. The aim of the present project is precisely twofold: 1) investigating and designing formal techniques for testability analysis and for diagnosability analysis in distributed concurrent discrete-event systems (modelled with label transition systems or with Petri nets); 2) developing a unifying framework for both testability and diagnosability analysis and implementing a tool according to this framework.

This is a mobility project financed by the STIC-Amsud.

Coordinating Team