please refer to:
IFSTTAR website: www.ifsttar.fr
ESTAS team website: http://www.inrets.fr/linstitut/unites-de-recherche-unites-de-service/estas/
Beginning: between October and November 2012
Deadline for application: ASAP
Salary: 2500 € / month
Applicants should send the following documents to mohamed.ghazel@ifsttar.fr
- Detailed CV
- Motivation Letter
- PhD diploma ou any justification
- 2 or 3 more significant publications
- Recommendation letters + reference contacts
- Any additional element which may back the application
Contact:
Mohamed GHAZEL
IFSTTAR/ESTAS
20 rue Elisée Reclus
59666 Villeneuve d’Ascq
@: mohamed.ghazel@ifsttar.fr
Tel: +33.3.20.43.83.93
Deadline: August 31st 2012
Mission :
Railway - embedded control is becoming more and more complex due to the increasing integration of new features. In this context, and to fulfill the performance, comfort and safety goals, developing effective monitoring techniques becomes essential from the design phase of the system. In particular, having powerful tools of train onboard diagnosis is of a great interest since this minimizes, or even prevents, downtime by identifying failures effectively.
The results obtained through several projects have shown that the more the embedded railway control architecture becomes integrated and flexible, the more complex the treatment of safety issues becomes. Hence, developping effective monitoring techniques becomes essential from the design phase. One issue that must be addressed as part of the surveillance is that of diagnosability. Studying the diagnosability of a system intends to determine whether any predetermined failure can be detected and identified in a finite delay after its occurrence. Then comes the issue of developing a diagnoser which performs the diagnostic task, strictly speaking. The diagnoser's role is to determine, online, whether the behaviour of the monitored system is abnormal, and if so to determine the failure.
The partial observability is a typical issue that the diagnosis procedure has to handle. Actually, in embedded railway control, it is often quite expensive and technically difficult to fit the system so that one can detect any changes that may occur and gather any information necessary for supervision. Therefore, it becomes vital to develop efficient methods able to fill this partial observability on the system behaviour.
At a high level of abstraction, discrete models are more suitable for diagnosis studies than continuous models (Lin, 1994). Thus, the work to be carried out uses, in the main, discrete behavioural models.
The benefit of analyzing the diagnosability properties is twofold: during the design phase, the study of diagnosability can guide the sensors' placement and provide the degraded operation modes. On the other hand, diagnosability properties may guide online the reconfiguration process following the recognition of an abnormal behaviour.
Early works on the diagnosis field offer non-constructive definitions of diagnosability, as in (Sampath et al., 1995). Such definitions formulate when a system is said to be diagnosable, but do not explain how to decide if a model is diagnosable in a straightforward way. Later, the model-checking techniques have been used in (Cimatti et al., 2003), (Huang et al., 2004) and (Grastien, 2009), to become more and more close to an operative definition. Nevertheless, all these works have in common the need for intermediate models, before they can roll out the model-checking. Thus, none of these works really completes an operative definition: that is to say definition with a clear semantics describing how to explore the behaviour, in order to investigate the diagnosability of the system.
As part of this mission, we wish to develop formulations for diagnosability and diagnosis issues pertinent to embedded railway control applications. Having such formulations allows us to take advantage of formal verification techniques (mainly model checking) in order to solve these problems and to be able to handle complex shapes of failures (particular sequences of events, lack of response, constraints on the occurrence time of events). Also, on the basis of these formulations, we intend to develop mechanisms for sensors' placement while taking into account time information. Moreover, and given that recent works on symbolic techniques (SAT techniques) have shown a big efficiency in the implementation of verification algorithms, we wish to study the contribution of these techniques in terms of performance. This question is crucial since we consider complex systems in which the combinatorial explosion problem is inherent.
Profil des candidats :
Having good skills in formal methods, discrete event models and software engineering.
Backrgound in diagnosis of discrete event models or/and railway application will be appreciated.