Friday, 24 May 2013

Post-doc position in LAAS-CNRS, Toulouse (model checking & testing)


Post-doc position on
Structural analysis of counterexamples


A key issue in model checking is how to locate faults that caused property violation, when a lengthy counterexample is returned. Previous work done in collaboration with Airbus [Boc10] has addressed this issue in the framework of Scade or Simulink design models. The approach is based on a structural analysis that identifies paths of the model that are activated by a counterexample over time. This analysis allows the extraction of relevant information to explain the observed violation. It may also serve to guide the model checker toward the search for different counterexamples, exhibiting new path activation patterns and thus new ways to violate the property. The aim is to give engineers as much usable feedback as possible before a fix is attempted. The approach has been implemented in a tool called STANCE (Structural ANalysis of CounterExamples). It is closely related to path-based analysis techniques developed for structural testing.

The objective of this post-doc is to further elaborate the approach. A first direction concerns the extraction of explanatory information from the execution of a counterexample. The current algorithm focuses on the traversal Boolean and temporal operators. Work will consider an extension to handle numerical operators as well. A second direction is on the definition and comparison of strategies for obtaining new counterexamples. The simple strategy implemented in STANCE provided a first assessment of the feasibility and potential interest of the idea. A systematic investigation of more elaborated path-based strategies is now needed, with possibly a combination of symbolic and heuristic techniques.

[Boc10] T. Bochot, P. Virelizier, H. Waeselynck, V. Wiels. Paths to Property Violation: A Structural Approach for Analyzing Counter-Examples. In Proc. HASE 2010.
http://doi.ieeecomputersociety.org/10.1109/HASE.2010.15


Practical information

The post-doctoral position is funded by RTRA STAE, the French space and aeronautic sciences & technologies foundation, as part of the IFSE project on formal system engineering. It is located in Toulouse, a nice city in the heart of Southern France. Toulouse is famous for its aeronautical and space achievements, its university founded in 1229, its laboratories and research centers.


The position is open at LAAS-CNRS, in the "Dependable Computing and Fault Tolerance" Group (http://www.laas.fr/TSF-EN/). Work will be done in collaboration with ONERA (http://www.onera.fr/dtim-en/critical-systems/index.php). Gross salary is between 2500 and 3000 euros per month. Post-doc will start between September and December 2013 for a duration of one year.

Qualifications

PhD in computer science.
Expertise in model checking or testing techniques necessary.
Knowledge of Scade/Simulink or more generally data flow languages welcome.

Application

Candidates should send a resume and recommendation letters via email to: Helene.Waeselynck@laas.fr and Virginie.Wiels@onera.fr

--------------------------------------------------------------
Helene Waeselynck           E-mail: Helene.Waeselynck@laas.fr
LAAS-CNRS                   tel: +33 (0)5 61 33 64 07
7, Av du Colonel Roche      fax: +33 (0)5 61 33 64 11
F-31400 Toulouse            http://homepages.laas.fr/waeselyn/
--------------------------------------------------------------

No comments:

Post a Comment