Journée du 24 Septembre 2010

Lieu

LACL, salle I 222, bâtiment I,: comment y aller
le bâtiment I est celui sous lequel on passe sur la dalle en venant du métro Créteil Université.

Programme

14h00-15h00: Thomas Robert, LTCI/Telecom ParisTech, "Moniteur d'exécution formel et tolérance aux Fautes Pratique"

Abstract: Nous présenterons une classe de détecteurs d'erreurs pouvant être générés à partir de modèles formels selon le principe de l'observateur. La particularité de ces détecteur réside dans la possibilité de les confronter à des modèles de propagation des fautes usuels pour en évaluer l'efficacité.

La démarche visant à générer un détecteur d'erreur, à des fins de mise au point, à partir d'une spécification formelle est désormais relativement commune [1]. Cependant, ce type de mécanisme n'est jamais, ou très rarement, déployé en phase opérationnelle pour des systèmes critiques. La raison principale de leur retrait réside dans leur coût en l'absence de fautes, et la difficulté à évaluer leur efficacité en termes de détection effective d'erreur correspondant à des fautes classiques [2]. Nous verrons ensuite une démarche permettant de confronter ces détecteurs aux modèles utilisés pour évaluer la propagation des erreurs au sein d'un système. Cette confrontation permet de confronter le modèle d'occurrence des fautes et de leur manifestation avec l'implémentation du détecteur d'erreurs. En particulier, l'architecture nécessaire à la synchronisation entre le moniteur et le système sera précisée en gardant à l'esprit l'objectif de confinement des erreurs.

[1] Delgado, N., Gates, A. Q., and Roach, S. 2004. A Taxonomy and Catalog of Runtime Software-Fault Monitoring Tools. IEEE Trans. Softw. Eng. 30, 12 (Dec. 2004), 859-872. DOI= http://dx.doi.org/10.1109/TSE.2004.91

[2] Pascal Chevochot, Isabelle Puaut, "Experimental Evaluation of the Fail-Silent Behavior of a Distributed Real-Time Run-Time Support Built from COTS Components," International Conference on Dependable Systems and Networks, p. 0304, 2001

15h00-15h30 : Lukasz Fronc, IBISC "compilation optimisée de réseaux de Petri"

Abstract: Nous présentons un cadre formel pour la compilation optimisée de réseaux de Petri colorés, utilisée pour accélérer l'exploration d'espaces d'états explicites. Ce cadre formel nous permet de définir un compilateur et de prouver l'intégralité du code qu'il génère. Ce compilateur a été prototypé et nous montrons par une comparaison avec l'outil Helena (qui fait aussi de la compilation et de l'exploration explicite) que les optimisations considérées apportent une accélération substantielle..

15h30-16h00: pause café

16h00-16h30: vie du groupe