OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Détection d'erreur au plus tôt dans les systèmes temps-réel : une approche basée sur la vérification en ligne

Robert, Thomas. Détection d'erreur au plus tôt dans les systèmes temps-réel : une approche basée sur la vérification en ligne. PhD, Institut National Polytechnique de Toulouse, 2009

[img]
Preview
(Document in French)

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
2MB

Official URL: http://ethesis.inp-toulouse.fr/archive/00000868/

Abstract

La vérification en ligne de spécifications formelles permet de créer des détecteurs d'erreur dont le pouvoir de détection dépend en grande partie du formalisme vérifié à l'exécution. Plus le formalisme est puissant plus la séparation entre les exécutions correctes et erronées peut être précise. Cependant, l'utilisation des vérifieurs en-ligne dans le but de détecter des erreurs est entravée par deux problèmes récurrents : le coût à l'exécution de ces vérifications, et le flou entourant les propriétés sémantiques exactes des signaux d'erreur ainsi générés. L'objectif de cette thèse est de clarifier les conditions d'utilisation de tels détecteurs dans le cadre d'applications « temps réel » critiques. Dans ce but, nous avons donné l'interprétation formelle de la notion d'erreur comportementale « temps réel». Nous définissions la propriété de détection « au plus tôt » qui permet de d'identifier la classe des détecteurs qui optimisent la latence de détection. Pour illustrer cette classe de détecteurs, nous proposons un prototype qui vérifie un comportement décrit par un automate temporisé. La propriété de détection au plus tôt est atteinte en raisonnant sur l'abstraction temporelle de l'automate et non sur l'automate lui-même. Nos contributions se déclinent dans trois domaines, la formalisation de la détection au plus tôt, sa traduction pour la synthèse de détecteurs d'erreur à partir d'automate temporisés, puis le déploiement concret de ces détecteurs sur une plate-forme de développement temps réel, Xenomai.

Item Type:PhD Thesis
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut National Polytechnique de Toulouse - INPT
Laboratory name:
Research Director:
Fabre, Jean-Charles
Statistics:download
Deposited By: admin admin

Repository Staff Only: item control page