|
Département d'ingénierie informatique |
Project leader : C. Pecheur
Collaborations :
- A. Cimatti (IRST, Italy),
- T. Mens (Service de Génie logiciel, UMH, Belgium),
- M. Lowry (NASA Ames, USA),
- F. Raimondi (University College London, UK).
Description :
Programmed controllers are more and more pervasive in our environment, from nuclear plants down to cellular phones. In particular, these controllers can be in charge of detecting, diagnosing and recovering from potential failures in the controlled system. This is a complex task because the controller has a partial and indirect view of the state of the system, and the number of possible situations increases exponentially with the size of the system. The goal of this activity is to develop methods and tools to analyze and verify the fault protection properties of a system, and more generally reason on systems in terms of partial observability. To this end, we are using a powerful analysis technique called symbolic model checking, that can exhaustively explore very large state spaces.
This activity builds on five years of applied research lead by Charles Pecheur at NASA Ames in California, where these techniques were targeted at model-based diagnosis applications designed for space missions. A translator has been developed to feed models to a symbolic model checker, and real-size applications (up to more than 10exp50 states) have been successfully analyzed through that path.
With Charles Pecheur's arrival at UCL a couple months ago, this line of work is only now restarting and seeking funding, and has not yet resulted in significant achievements for UCL. We are looking into different directions to expand our activities:
- Realistic case studies - with our NASA partners and others, in order to assess scalability and relevance of our approach.
- Real-time and hybrid models - generalizing from the discrete, finite-state models we have addressed so far.
- Technology maturation and transfer - producing user-friendly and robust tools that engineers can use.
- Man-machine interfaces - those systems feature similar partial observability concerns as found in diagnosis.
- Risk analysis - use model-checking techniques to analyze or even generate risk-related artifacts such as fault trees.
- Modal logics - observability can be seen as a particular case of more expressive logics, such as epistemic logic or game-theoretic logics.
The translator (developed at NASA Ames)
takes models and specifications used in diagnosis applications (Livingstone),
feeds them into a powerful symbolic model checker (SMV) and translates
the results back in terms of the original model, altogether providing
powerful analysis and verification technology for Livingstone-based
applications.