Constellation, le dépôt institutionnel de l'Université du Québec à Chicoutimi

Résumé

L’event stream processing (ESP) est le traitement d’un flux continu d’objets, appelé séquence d’événements, dans l’optique de l’analyser ou de le transformer. Le laboratoire d’informatique formelle de l’UQAC (LIF) développe depuis plusieurs années un moteur de stream processing open source appelé BeepBeep 3. Cet engin permet une utilisation facile du concept d’ESP. À BeepBeep 3, on y a intégré un système de vérification formelle. Avec seulement quelques lignes de code supplémentaires, il est maintenant possible de générer automatiquement une structure de Kripke d’une chaîne de processeurs donnée. Des applications intéressantes s’ajoutent donc à l’utilité déjà vaste de BeepBeep. Comparer des pipelines à l’aide de formules en logique temporelle linéaire (LTL) ou en logique du temps arborescent (CTL) et l’idée qu’une chaîne de processeurs monitore une structure de Kripke ne sont que quelques exemples. Dans ce mémoire, on expliquera tout le processus de réflexion et d’exécution qui a mené à l’automatisation de la construction d’une chaîne de processeur BeepBeep en un modèle de Kripke valide pour analyse dans le logiciel NuXMV.