Experimentations de techniques de verification de proprietes temps reel sur un systeme de controle de train d'atterrissage

摘要

Cet article presente les resultats d'un ensemble d'experiences visant a etudier differentes techniques de verification formelle de proprietes temps reel sur une etude de cas, issue du domaine avionique. Cette etude de cas est une simplification du systeme de controle des trains d'atterrissage d'un avion du type Rafale. Ce systeme est compose de trois trains differents, qu'il s'agit de commander en fonction des ordres du pilote (ordre de descente ou de remontee des trains) au moyen d'un ensemble d'actionneurs (electrovannes...). Ce systeme, dont le coeur est realise en logiciel, a ete specifie dans trois langages formels differents: Esterel [2, 3], Lustre [4, 6], puis le formalisme des automates temporises [1]. L'interet de ces trois langages est d'offrir la possibilite d'utiliser des techniques de verification automatique appelees " model checking ". Seules deux proprietes (c'est-a-dire des exigences de bon comportement), jugees difficiles, ont ete etudiees sur le systeme ainsi specifie a l'aide de trois outils de verification. La demonstration de ces deux proprietes a ete realisee avec succes et automatiquement par un de ces trois outils, le " Model Checker" SMV ([10,14]) travaillant sur Lustre. Les autres outils ont echoue, en particulier UPPAAL [16] (automates temporises) consideres pourtant comme un des plus efficaces du domaine des automates temporises. Cette experimentation permet de montrer l'etat d'avancement et les difficultes encore rencontrees dans le domaine de la verification des logiciels embarques.