Abstract FR:

Dans cette these, nous presentons de nouvelles techniques et de nouveaux outils developpes autour du langage reactif electre pour la verification et l'execution d'applications temps-reel de taille industrielle, et en particulier d'une application de controle-commande d'un turboreacteur. Nous nous interessons d'abord a la verification d'automates hybrides lineaires, un modele adapte aux applications temps-reel. En particulier, nous etudions des problemes d'explosion de l'espace des etats auxquels nous sommes confrontes en raison de la taille importante des applications que nous devons traiter. Pour resoudre ces problemes, nous proposons une technique d'approximation : l'analyse separee d'accessibilite. Un programme electre est compile en un fiffo-automate, son modele d'execution. A des fins de verification, nous decrivons les demarches de traduction du fiffo-automate en un automate d'etats fini et en un automate hybride lineaire. Puis, de facon a pallier des problemes d'explosion combinatoire pouvant survenir dans la composition d'automates, nous proposons des demarches de reduction de modeles, dont une technique de reduction par temporisation. Nous detaillons ensuite une implementation du fiffo-automate et nous presentons deux logiciels permettant la mise en uvre pratique des techniques precedentes, dont un outil de verification d'automates hybrides lineaires appele pollux. Nous illustrons l'utilisation de ces techniques et de ces outils sur l'application de controle-commande. Nous commencons par programmer en electre les aspects reactifs de l'application. Puis, nous construisons les modeles des programmes sur lesquels nous verifions des proprietes de surete. Enfin, nous presentons la demarche d'integration des programmes electre dans l'application en vue de les executer.