A comprehensive method for the verification of real-time requirements : application to integrated modular avionics

Dans le domaine de l’aéronautique, les systèmes embarqués ont fait leur apparition durant les années 60, lorsque les équipements analogiques ont commencé à être remplacés par leurs équivalents numériques. Dès lors, l’engouement suscité par les progrès de l’informatique fut tel que de plus en plus de fonctionnalités ont été numérisées. L’accroissement permanent de la complexité des systèmes a conduit à la définition d’une architecture appelée Avionique Modulaire Intégrée (IMA pour Integrated Modular Avionics). Cette architecture se distingue des architectures antérieures, car elle est fondée sur des standards (ARINC 653 et ARINC 664 partie 7) permettant le partage des ressources de calcul et de communication entre les différentes fonctions avioniques. Ce type d’architecture est appliqué aussi bien dans le domaine civil avec le Boeing B777 et l’Airbus A380, que dans le domaine militaire avec le Rafale ou encore l’A400M. Pour des raisons de sûreté, le comportement temporel d’un système s’appuyant sur une architecture IMA doit être prévisible. Ce besoin se traduit par un ensemble d’exigences temps réel que doit satisfaire le système. Le problème exploré dans cette thèse concerne la vérification d’exigences temps réel dans les systèmes IMA. Ces exigences s’articulent autour de chaînes fonctionnelles, qui sont des séquences de fonctions. Une exigence spécifie alors une borne acceptable (minimale ou maximale) pour une propriété temporelle d’une ou plusieurs chaînes fonctionnelles. Nous avons identifié trois catégories d’exigences temps réel, que nous considérons pertinentes vis-à-vis des systèmes étudiés. Il s’agit des exigences de latence, de fraîcheur et de cohérence. Nous proposons une modélisation des systèmes IMA, et des exigences qu’ils doivent satisfaire, dans le formalisme du tagged signal model. Nous montrons alors comment, à partir de ce modèle, nous pouvons générer pour chaque exigence un programme linéaire mixte, c’est-à-dire contenant à la fois des variables entières et réelles, dont la solution optimale permet de vérifier la satisfaction de l’exigenceEmbedded systems appeared in aeronautics during the 60’s, when the process of replacing analog devices by their digital counterpart started. From that time, the broad thrust of computer science advances make it possible to digitize more and more avionics functionalities. The continual increase of the complexity of these systems led to the definition of a new architecture called Integrated Modular Avionics (IMA). This architecture stands apart from previous architecture because it is based on standards (ARINC 653 and ARINC 664 part 7) which allow the sharing of computation and communication resources among avionics functions. This architecture is implemented in civil aircrafts, with Boeing B777 and Airbus A380, and in military aircrafts, with Rafale or A400M. For safety reason, the temporal behaviour of such a system must be predictable, which is expressed with a set real-time requirements. A real-time requirement specifies an upper or lower bound of a temporal property of one or several functional chains. A functional chain is a sequence of functions. In this thesis, we explore the verification of real-time requirements in IMA systems. We have identified three real-time requirements relevant to our problem : latency, freshness and consistency. We propose a model of IMA systems, and the requirements they must meet, based on the tagged signal model. Then we derive from this model, for each requirement, a mixed integer linear program whose optimal solution allows us to verify the requiremen