Détails sur le séminaire

Résumé : La conception à base de composants est le processus qui permet à partir d’exigences et un ensemble de composants prédéfinis d’aboutir à un système respectant les exigences. Les composants sont des blocs de construction encapsulant du comportement. Ils peuvent être composés afin de former des composants composites. Leur composition doit être rigoureusement définie de manière à pouvoir i) inférer le comportement des composants composites à partir de leurs constituants, ii) déduire des propriétés globales à partir des propriétés des composants individuels. Cependant, il est généralement impossible d’assurer ou de vérifier les propriétés souhaitées en utilisant des techniques de vérification statiques telles que la vérification de modèles ou l’analyse statique. Ceci est du au problème de l’explosion d’espace d’états et au fait que la propriété est souvent décidable uniquement avec de l’information disponible durant l’exécution (par exemple, provenant de l’utilisateur ou de l’environnement).
La vérification à l’exécution (Runtime Verification) désigne les langages, les techniques, et les outils pour la vérification dynamique des exécutions des systèmes par rapport à des propriétés spécifiant formellement leur comportement. En vérification à l’exécution, une exécution du système vérifiée est analysée en utilisant une procédure de décision : un moniteur. Un moniteur peut être généré à partir d’une spécification écrite par l’utilisateur (par exemple une formule de logique temporelle, un automate) et a pour but de détecter les satisfactions ou les violations par rapport à la spécification. Généralement, le moniteur est une procédure de décision réalisant une analyse pas à pas de l’exécution capturée comme une séquence d’états du système, et produisant une séquence de verdicts (valeur de vérité prise dans un domaine de vérité) indiquant la satisfaction ou la violation de la spécification.
Cette thèse s’intéresse au problème de la vérification de systèmes à composants multithread et distribués. Nous considérons un modèle général de la sémantique et système à composants avec interactions multi-parties: les composants intrinsèquement indépendants et leur interactions sont partitionées sur plusieurs ordonnanceurs. Dans ce contexte, il est possible d’obtenir des modèles avec différents degrés de parallelisme, des systèmes séquentiels, multi-thread, et distribués. Cependant, ni le modèle exact ni le comportement du système est connu. Ni le comportement des composants ni le comportement des ordonnanceurs est connu. Notre approche ne dépend pas du comportement exact des composants et des ordonnanceurs. En s’inspirant de la théorie du test de conformité, nous nommons cette hypothèse : l’hypothèse de monitoring. L’hypothèse de monitoring rend notre approche indépendante du comportement des composants et de la manière dont ce comportement est obtenu. Lorsque nous monitorons des composants concurrents, le problème qui se pose est celui de l’indisponibilité de l’état global à l’exécution. Une solution naïve à ce problème serait de brancher un moniteur qui forcerait le système à se synchroniser afin d’obtenir une séquence des états globaux à l’exécution. Une telle solution irait complètement à l’encontre du fait d’avoir des exécutions concurrentes et des systèmes distribués. Nous définissons deux approches pour le monitoring de système un composant multi-thread et distribués. Dans les deux approches, nous attachons des contrôleurs locaux aux ordonnanceurs pour obtenir des événements à partir des traces locales. Les événements locaux sont envoyés à un moniteur (observateur global) qui reconstruit l’ensemble des traces globale qui sont i) compatibles avec les traces locales et ii) adéquates pour le monitoring, tout en préservant la concurrence du système.
Monitoring des systèmes à composants multi-thread. Tout d’abord, nous nous intéressons aux problèmes du monitoring en ligne de propriétés temporelles linéaire et indépendantes de leur logique de spécification. Nous considérons des systèmes à composants multi-threads décrits dans le framework BIP (Behavior Interaction Priority), dans lequel les interactions peuvent être exécutées de manière concurrentes avec un ordonnanceur central pour les interactions multi-partie. BIP est un cadre expressif pour la construction formelle de systèmes hétérogènes. Notre technique reconstruit à la volée les états globaux par accumulation des états partiels traversés par le système lors de son exécution. Nous définissons des transformations de composants qui préservent leur sémantique et leur concurrence, et qui à la fois permet de vérifier des propriétés sur les états globaux. Nous présentons RVMT-BIP, un outil prototype implémentant les transformations pour le monitoring de système BIP. Nos expérimentation sur plusieurs systèmes BIP démontrent que RVMT-BIP n’induit qu’une faible dégradation des performances.
Monitoring des systèmes à composants distribués. Deuxièmement, nous nous intéressons au problème du monitoring des systèmes à composants avec interaction multi-partie pour des propriétés exprimées en logique linéaire temporelle qui font référence aux états globaux. Dans ce contexte, la reconstruction des traces globales est faite à la volée en utilisant un treilis des états partiels encodant les traces globales qui sont compatibles avec les traces observés localement. Nous avons implémenté notre approche de monitoring dans un outil prototype appelé RVDIST. RVDIST s’exécute en parallèle avec le modèle distribué et prend en entrée les événements générés par chacun des ordonnanceurs et produit le treillis des exécutions. Nos expérimentations démontrent que, grâce a l’optimisation appliquée dans l’algorithme de monitoring en ligne, (i) la taille du treillis construit ne dépend pas du nombre d’événements reçus, (ii) la taille du tri est raisonnable, (iii) l’impact en terme de performance du processus de monitoring est faible.