La spécification, la programmation et la vérification de systèmes critiques ont fait l’objet d’importants efforts de recherche. Le domaine des systèmes interactifs, et plus particulièrement celui des applications logicielles interactives critiques, n’a pas du tout bénéficié des mêmes efforts. Or, paradoxalement, l'accidentologie aéronautique fait clairement apparaître que le bon fonctionnement de ces applications est mis en cause de manière récurrente dans l'ensemble des accidents ou incidents recensés. La thèse analyse d'abord les causes de ce paradoxe et de cet état de fait. Cette analyse conduit à formuler et détailler un ensemble d’exigences pour une nouvelle approche de spécification et conception de ces applications. La thèse propose ensuite, en s'inscrivant dans la recherche de réponses satisfaisantes à ces exigences, les bases d'un langage permettant de décrire la composition et le comportement attendu de ces applications. Pour ce faire, un modèle d’architecture de systèmes interactifs est avancé. Il se fonde sur des composants de base, les interacteurs, et décrit, les concernant, les notions d'abstraction et de composition de systèmes. Le langage LIDL (LIDL Interaction Description Language), proposition centrale de la thèse, permet de décrire formellement les interacteurs de ce modèle. Leur composante statique est décrite sous la forme d’interfaces. Leurs composantes dynamiques sont décrites sous la forme d’interactions. Une description LIDL se construit sur un ensemble réduit d’interactions de base ainsi que sur quelques constructeurs du langage permettant de les composer. LIDL est un langage à flot de données synchrones qui décrivent les interactions. Les flots intègrent une donnée d’activation, qui dénote la présence ou l’absence de valeur du flot. La compilation de descriptions LIDL permet de produire des machine d'états se prêtant bien aux techniques de vérification formelle. L’adéquation de l’approche et du langage proposés avec les exigences identifiées au départ est finalement examinée à travers leur mise en œuvre sur un cas d'étude.
Vincent Lecrubier (Tue,) studied this question.