Abstract FR:

Dans le domaine de l'analyse de surete des systemes programmes, intervenant dans la protection des centrales nucleaires reparties sur le territoire francais, le commissariat a l'energie atomique (cea) s'interesse aux methodes de validations par tests, appliquees aux composants logiciels de ces systemes. Ces tests sont effectues par des simulations logicielles selon des scenarios pre-etablis concus par des specialistes. L'equipe de validation souhaite alors verifier que certaines proprietes cruciales sont toujours respectees. Ces verifications peuvent avoir lieu pendant ou apres l'execution simulee du logiciel. Ces simulations evenementielles portent sur des applications temps reel de type flots de donnees (dataflow). Un important travail de formalisation etait necessaire pour decrire dans un langage textuel suffisamment lisible, expressif et exploitable pour tout ou parties des categories de proprietes informellement exprimees par les valideurs sur des exemples modeles. Les proprietes suggerees font intervenir des aspects temporels, des questions d'ordonnancement d'evenements repetitifs et des intervalles de temps. Cette these se propose de definir le langage efri. Il est oriente flots de donnees et generalise, du point de vue semantique, les formalismes bases sur les logiques temporelles d'intervalles. Nous decrivons un procede semblable a une compilation, rendant plus efficace l'evaluation des formules de notre langage. Base sur un formalisme de type expressions rationnelles vectorielles, notre procede de compilation ramene la verification d'une propriete, exprimee par une formule du langage logique efri, au probleme de l'appartenance d'un mot a un langage rationnel, mecaniquement construit a partir de cette formule