Runtime Verification of Real-Time Applications Using Trace Data and Model Requirements

Surveiller les systèmes multi-cœurs est difficile en raison des processus s'exécutant en parallèle, et pouvant interférer les uns avec les autres lorsqu'il s'agit d'accéder aux ressources du système, ou simplement d'avoir du temps processeur. Un tel système peut avoir à suivre des principes temps réel, ajoutant des contraintes de temps qui invalident les résultats dès qu'une date limite est manquée. Sur ce genre de système, des données précises n'auront ainsi de valeur que si elles peuvent être produites en respectant un délai donné. Le traçage peut fournir une grande quantité d'informations d'exécution de haute précision, à la fois sur le système et les applications. Il est ainsi souvent l'outil le plus précis et fiable pour étudier et analyser des systèmes ainsi contraints. Cependant, les utilisateurs doivent disposer d'une grande expertise du système afin de comprendre les évènements du noyau du système et leur signification. De plus, il peut être très long d'analyser et étudier manuellement de volumineuses traces d'exécution de haute précision.

Dans cette thèse, nous proposons les méthodes et algorithmes permettant d'automatiquement détecter et identifier l'origine de comportements inattendus dans des applications, et ce à l'aide de traces de leurs exécutions et de modèles des exigences. Nous décrivons la structure interne des modèles, la méthodologie pour suivre l'exécution d'une application à travers ses évènements de l'espace utilisateur, et les structures de données nécessaires pour vérifier les contraintes. Nous détaillons ensuite le processus utilisé pour détecter et finalement comprendre la source du comportement non désiré. Nous proposons aussi une approche pour construire automatiquement les modèles pour des applications temps réel courantes.

L'hypothèse servant de point de départ pour ce travail est que les traces d'exécution du système et de l'application à analyser peuvent être utilisées pour automatiquement suivre l'exécution de cette application, y détecter les anomalies et trouver leurs sources.

Les résultats de ce travail sont les concepts, méthodologies et structures de données utilisés pour suivre et contraindre des applications, ainsi que les méthodes et algorithmes qui permettent de détecter et identifier les comportements inattendus dans ces applications. Ces derniers ont été testés sur de réelles applications temps réel, et ont permis avec succès de détecter et identifier l'origine des irrégularités à leur exécution. De plus, nous avons pu automatiquement, et de façon précise, construire des modèles pour ces applications. Cette dernière étape rend l'utilisation des méthodes de traçage beaucoup plus accessible aux utilisateurs non-experts.

Le résultat final est que la détection automatique et la localisation automatique de la source des comportements inattendus dans une application est une option viable et fonctionnelle, qui accélère et simplifie le travail des utilisateurs pour analyser les exécutions de leurs applications.