Vérification au moment de l’exécution (runtime monitoring)

Vérification au moment de l’exécution (runtime monitoring)

Actuellement, l’analyse, l’évaluation des performances et la garantie du bon fonctionnement des systèmes sont rendues des activités difficiles à cause de la complexité croissante des systèmes. Or, dans les dernières décennies, la traçabilité a démontré son utilité que ce soit pour identifier des problèmes de performance ou de fonctionnalité. Selon la norme ISO 8402, la traçabilité est : « l’aptitude à retrouver l’historique, l’utilisation ou la localisation d’un article ou d’activités semblables au moyen d’une identification enregistrée». Il s’agit donc d’une démarche qui consiste à donner la possibilité de retrouver la trace et les différents lieux de vie d’un produit. Parmi les fonctions de la traçabilité, la vérification des traces ou l’analyse des traces est considérée comme une étape cruciale.

Quel que soit le domaine, le principe de fonctionnement est toujours le même : on conserve la trace (aussi appelé log ou journal) de tous les événements produits par un système (transfert de fonds, entreposage ou transformation d’un item) pour éventuellement procéder à l’analyse du registre ainsi produit en cas de problème. Une trace informatique est l’ensemble des informations qui ont été conservées de l’exécution du système et qui permettent de savoir ce qui s’est produit. Elles peuvent être issues d’un traitement effectué par un utilisateur, un processus ou une application. La trace informatique prend des formes variées : lignes d’un fichier, événements d’un journal, entrées dans une base de données, informations dans l’application elle-même. Comme toute trace, sa qualité doit garantir une reconstitution exacte des événements et faire l’objet d’une analyse selon des critères. L’analyse des traces d’événements permet d’identifier des erreurs dans l’exécution du système ou la violation de certaines politiques .

Pour illustrer l’intérêt de l’analyse de traces, nous allons donner deux exemples. Le premier exemple est celui des services web. Prenons l’exemple d’un individu qui désire effectuer un voyage. Pour ce faire, il voudra acheter tous les services nécessaires à ce périple sur la page web de son agence de voyages. Ce scénario se compose de quatre entités : un client, une agence de voyages, une compagnie aérienne et une chaîne d’hôtels. La Figure 1.1 représente ces entités, ainsi que leurs interactions possibles. Un client effectue d’abord une requête pour s’informer des vols et des chambres d’hôtel, puis valide une réservation. L’agence de voyages reçoit et traite cette requête et le transmet à la compagnie aérienne et à la chaine d’hôtels. Ces deux dernières répondent aux requêtes de l’agence de voyages pour réserver des places sur ces vols et des chambres dans ses hôtels. Dans ce scénario, une trace d’événements correspond aux différentes requêtes et réponses échangées entre ces entités. Plusieurs contraintes peuvent devoir s’appliquer dans ce scénario. Par exemple : 1- Si l’agent client demande un forfait, alors il recevra éventuellement la liste des vols et des hôtels. 2- Dans chaque exécution, il est toujours vrai que l’annuaire de l’hôtel est finalement interrogé. Si ces deux contraintes sont violées, alors il existe une anomalie dans l’interaction entre les entités et un message d’erreur doit être envoyé au client.

Un deuxième exemple est considéré dans le même contexte, celui de l’interface Iterator de Java. Cette interface fournit des méthodes pour effectuer un parcours séquentiel d’une structure de données. L’interface offre principalement deux méthodes : hasNext et next. La première renvoie un booléen qui indique si le parcours de la structure de données est achevé. La seconde renvoie l’objet suivant de la structure de données. L’interface Iterator exige cependant que la méthode hasNext soit appelée et renvoie ‘True’ avant que la méthode Next ne soit appelée. La Figure 1.2 décrit une machine à états finis qui définit les interactions possibles entre les états. À partir de l’état ‘unknown’, il existe toujours une erreur en appelant la méthode Next. Si la méthode hasNext est appelée et renvoie6 True’, on peut dans ce cas appeler la méthode Next. Sinon, il n’y a plus des éléments et le moniteur passe à l’état ‘none’. Dans les états ‘more’ et ‘none\ l’appel de la méthode hasNext ne fournit aucune nouvelle formation. À partir de l’état ‘more\ il est acceptable d’appeler la méthode next et le moniteur retourne à l’état ‘unkown\ L’appel de la méthode ‘Nexf à partir de l’état ‘none’ rentre dans l’état ‘error’

Problématique et objectif

Les exemples précédents montrent l’importance de vérifier des propriétés sur des traces pour garantir le bon fonctionnement des systèmes. Or, l’analyse efficace de logs de grande taille est présentement un domaine incontournable, particulièrement si le contrat à vérifier inclut des contraintes sur les paramètres des événements. Mis à part quelques algorithmes ad hoc, il existe peu d’outils répandus permettant de vérifier des propriétés complexes sur des traces d’événements. Un bon analyseur de traces doit répondre à un certain nombre de besoins. D’abord, il doit permettre de trouver des séquences complexes dans une trace, qui invoquent plusieurs événements séparés dans le temps et plusieurs paramètres à l’intérieur de chacun. Son langage d’entrée doit donc être suffisamment riche pour permettre à l’utilisateur de spécifier ces séquences. Deuxièmement, l’analyseur de traces doit pouvoir fonctionner sur de grandes traces d’événements. Dans ce cas, il faut un système qui puisse traiter efficacement de grandes traces et qui se comporte de façon gracieuse par rapport à une augmentation de la quantité d’événements. Le temps et la mémoire requise pour traiter chaque événement individuel doivent demeurer à l’intérieur de bornes raisonnables. Or, si le procédé de journalisation des événements est généralement bien compris, les produits actuels n’offrent que des moyens primitifs d’analyser et de vérifier les traces d’événements qu’ils produisent. On peut, au mieux, filtrer la liste des événements pour ne conserver que ceux qui répondent à certains critères. Les exemples mentionnés précédemment montrent que les contraintes à respecter vont au-delà de tels filtres simplistes. Depuis une dizaine d’années, des logiciels d’analyses de traces et des prototypes ont été développés par des chercheurs. Notre revue de littérature a répertorié quatorze algorithmes et logiciels pouvant être employés à l’analyse de traces, et dont les domaines d’applications sont variés. Par exemple, BeepBeep (Halle, 2008) est utilisé dans le monitoring des services web; Monid (Naldurg et al, 2004) est un outil de détection des intrusions; SPIN (Holzmann, 1997) est un outil logiciel pour la vérification des modèles qui a permis la vérification effective de protocoles de communication et de programmes C; NuSMV (Cimatti et al., 2002) est un model checker conçu pour faire une vérification fiable des modèles de taille industrielle. A la lumière de cette étude bibliographique, on distingue quatre problèmes. 1- Chaque outil utilise un format différent pour les traces et les propriétés. À titre d’illustration, BeepBeep prend en entrée une trace dans un fichier XML et une propriété décrite en logique temporelle linéaire de premier ordre (LTL-FO+); SPIN prend en entrée un modèle décrit par le langage PROMELA et une propriété LTL . Aussi, NuSMV reçoit en entrée un modèle décrit par le langage SMV et les propriétés sont exprimées en logique temporelle (CTL, LTL). De plus, la conversion d’un langage à un autre n’est pas triviale. La conversion n’est pas limitée à une simple traduction syntaxique, mais est plutôt une conversion complète qui prend en considération les propriétés les plus spécifiques pour chaque fichier. On ne peut pas simplement rechercher les mots clés d’un tel langage et les remplacer dans l’autre langage. 2- La plupart des solutions existantes sont mal documentées en ce qui a trait à leur performance. Parmi tous les outils répertoriés, seuls BeepBeep et SPIN fournissent des données empiriques. Il est donc très difficile de savoir à quel point tel ou tel outil fonctionne bien. 3- La plupart des solutions existantes ont été développées pour une utilisation particulière : par exemple, BeepBeep a été développé pour monitorer des services web; NuSMV vérifie des machines à états finis. Même si plusieurs solutions pourraient être appliquées dans un autre scénario que celui pour lequel elles ont été conçues, il n’existe pas de bancs d’essai avec lesquels comparer les solutions de toute façon. 4- Dans la plupart des solutions existantes, le temps et la mémoire consommée varient beaucoup d’un scénario à l’autre, sans qu’il existe un consensus à savoir quelle méthode fonctionne « le mieux ». L’objectif de la présente recherche consiste à pallier à ce manque en faisant une étude comparative des outils et des algorithmes de vérification des traces.

Méthodologie

Pour atteindre l’objectif de la recherche, trois étapes ont été définies :
1- Inventorier les outils de validation des traces. Une revue exhaustive de la littérature scientifique dans le domaine de la vérification et la validation des traces est faite afin de dégager les principaux outils et algorithmes développés. En plus des logiciels et algorithmes « traditionnels », nous avons ajouté un moteur de bases de données relationnelles et deux model checkers.
2- Développer un banc d’essai permettant de comparer leur performance. Ceci implique de :
– Comprendre le fonctionnement de chaque outil,
– Développer un modèle de traces indépendant de la représentation de chacun,
– Traduire de /vers les formats d’entrées de chacun à partir de cette représentation.
3- Tester le banc d’essai en développant une banque des traces et des propriétés provenant de scénarios variés et réalistes.

Contexte de la recherche

Ce travail a été réalisé en collaboration avec l’entreprise Novum Solutions, établie à Lévis. Cette entreprise, qui se spécialise dans le développement de produits de gestion d’inventaire basés sur la technologie RFID (Radio Frequency IDentification), veut ajouter la valeur à ses produits en lui adjoignant des fonctions d’analyse des traces. Dans ce scénario particulier, les événements sont des commandes de configuration d’un lecteur RFID et des entrées-sorties d’un article dans un entrepôt. Par exemple, le système pourrait s’assurer que tous les items observés dans un entrepôt sont bien réapparus par la suite dans l’inventaire à leur destination. D’une manière plus générale, l’utilisateur du système pourrait soumettre n’importe quel patron de recherche, représentant une séquence d’événements correspondant à un scénario précis, et obtenir du système les éléments qui y correspondent, s’il y a lieu. Les résultats obtenus vont donc permettre à Novum Solutions d’intégrer, par la suite, l’outil le plus performant d’après les différents tests effectués durant le projet.

Organisation du document

Le présent mémoire est composé de six chapitres. Après ce premier chapitre d’introduction générale, qui vise à situer le mémoire dans son contexte et à présenter les différentes étapes de la méthodologie de recherche employée dans le cadre de ce projet, le chapitre 2 est consacré à la présentation des scénarios où la vérification des traces est nécessaire. On décrit en détail cinq scénarios tirés de la littérature, pour lesquels la vérification de traces est importante. De plus, on énonce un total de neuf propriétés à vérifier dans ces scénarios. Le chapitre 3 présente les différentes formes des traces. Il définit un modèle formel pour représenter les traces. Aussi, il présente des langages pour exprimer les propriétés. À la fin du chapitre, on revient sur les exemples de propriétés décrites dans le chapitre 2 et on les exprime suivant le langage de spécification approprié. Le chapitre 4 décrit les principaux outils d’analyse des traces d’événements. Cette introduction est nécessaire dans le développement du banc d’essai. Dans le chapitre 5, les outils et les algorithmes cités sont montés dans un banc d’essai (benchmark) où ils sont comparés à travers une série de tests représentatifs des scénarios présentés dans le chapitre 2. En particulier, on explique comment un problème de validation de traces pour un outil peut être traduit en un problème équivalent pour un autre. Une partie est réservée pour la discussion des résultats obtenus. Nous terminons ce travail de recherche par une conclusion générale dans le chapitre 6 qui récapitule les différentes contributions apportées par ce mémoire, démontre l’atteinte de l’objectif et propose diverses perspectives de recherche future. Les principales conclusions de ce travail sont : Le temps alloué pour la vérification des traces est proportionnel aux longueurs des traces. – À travers les différents tests que nous avons faits, les meilleures performances sont obtenues avec l’outil MonPoly. Les résultats préliminaires de ce projet de recherche ont fait l’objet d’un article scientifique publié à la conférence « 3rd International Conference on Runtime Verification 2012 » (Mrad et al., 2012): « A Collection of Transducers For Trace Validation », RV 2012, Istanbul, Turquie 25 – 28 sept 2012. Un second article sera soumis à la conférence EDOC 2013.

SCÉNARIOS DE VÉRIFICATION DES TRACES

Ce chapitre est une description de tous les scénarios et leurs contraintes qui seront utilisées ultérieurement dans le jeu de tests de notre banc d’essai. Nous allons considérer cinq scénarios tirés de la littérature:
• Bookstore: scénario d’un achat de livre, tiré de (Van der Aalst, 2011), utilisé pour la surveillance des flux de production, la gestion des processus d’affaires, la modélisation et l’analyse des processus.
• Amazon ECS: service fournissant un accès à des données d’Amazon et des données de commerce électronique, tiré de (Amazon e-commerce service, 2005).
• LLRP: protocole de configuration des lecteurs RFID, tiré de (EPC-Globel, 2007).
• Cycle générateur: scénario de vérification des étiquettes RFID (aussi appelé Tags RFID), tiré de la gestion des stocks en entrepôts.
• Nombre aléatoire, scénario synthétique développé pour valider les résultats obtenus avec les derniers scénarios.

Bookstore

Le processus bookstore (Van der Aalst, 2011) décrit un scénario d’achat de livres. Il a été utilisé dans les travaux de Van der Aalst, professeur à l’université de technologie Eindhoven, pour la spécification et la surveillance des flux de production et pour la gestion des processus d’affaires. Le réseau de Pétri de la Figure 2.1 décrit le scénario de bookstore. Ce scénario se compose de quatre entités : le client (Customer), la librairie (Bookstore), l’expéditeur (Shipper) et l’éditeur (Publisher). Dans ce scénario, les événements sont les différents messages d’interactions entre ces quatre entités. Ce processus est initié par un client passant une commande (événement place_c_order), cette commande est envoyée et gérée par la librairie (événement handle_c_order). La librairie transfère par la suite la commande du livre de votre choix à un éditeur (événement place_b_order). L’éditeur évalue la commande de la librairie (événement eval_b_order) ; cette commande est soit acceptée (b_accept)5 soit rejetée (b_reject). Dans les deux cas, une réponse est envoyée à la librairie. Si la librairie reçoit une réponse négative, elle décide (événement decide) soit de rechercher un éditeur alternatif (événement alt_publ), soit de rejeter la commande du client (événement c_reject). Si la librairie recherche un éditeur alternatif, une nouvelle commande est envoyée au nouvel éditeur. Si le client reçoit une réponse négative (événement rec_decl), alors le processus est terminé. Si la librairie reçoit une réponse positive (événement c_accept), le client est informé (événement rec_acc) et la librairie continue le traitement de la commande du client. La librairie envoie une requête à un expéditeur (événement req__shipment) et l’expéditeur évalue la demande (événement eval_s_req), soit il accepte (événement s_accept), soit il rejette la demande (événement b_re j ect). Si la librairie reçoit une réponse négative, elle cherche un autre expéditeur. Ce processus est répété jusqu’à ce que l’expéditeur accepte. Une fois l’expéditeur trouvé, l’éditeur est informé (événement inf orm_publ), l’éditeur prépare le livre pour l’expédition (événement prepare_b) et le livre est envoyé de l’éditeur à l’expéditeur (événement send_ book). L’expéditeur prépare l’envoi au client (événement prepare_s) et envoie le livre au client (événement ship). Le client reçoit le livre (événement rec_book) et l’expéditeur avise la librairie (événement notify). La librairie envoie la facture au client (événement send_bill). Après avoir reçu à la fois le livre et la facture (événement rec_bill), le client effectue un paiement (événement pay). Puis la librairie traite le paiement (événement handle_payment) et le processus se termine.

Plusieurs contraintes sur l’ordre possible des événements peuvent se vérifier sur ce scénario. Par exemple: PI : L’événement « rec_acc» ne peut pas se produire à moins qu’un événement « place_c_orde r » n’ait été vu précédemment. P2 : Au moins une commande du client doit être éventuellement acceptée par la librairie.

Amazon E-Commerce web service

Les Amazon web services sont des services Amazon qui permettent d’accéder directement à la plateforme technologique Amazon. Les utilisateurs du service demandent des données à l’aide du protocole SOAP et les données sont renvoyées par le service  sous la forme d’un flux de texte au format XML. Parmi les services web d’Amazon, on compte S3 (Amazon Simple Storage Service) fournissant un stockage basé sur les services web, SES (Amazon Simple Email Service), service d’envoi en nombre et transactionnel d’emails, SQS {Amazon Simple Queue Service), fournissant une file de messages hébergé pour les applications web, etc. Le scénario qui nous intéresse ici s’appelle l’Amazon E-Commerce Service (AWS-ECS). C’est un service fournissant un accès aux données produits d’Amazon et des données de commerce électronique. Ce scénario a été utilisé dans les travaux de Halle (Halle et al.,2010). On considère le processus d’un panier de la Figure 2.2: Figure 2.2: Événements observés dans le scénario AWS – ECS. Ce scénario est initié par la création d’un panier (événement CREATE CART). Ensuite, des éléments peuvent être ajoutés dans ce panier (événement CART ADD). Enfin, ce panier peut être vérifié (événement CHECK OUT) . La Figure 2.2 décrit un scénario simplifié d’AWS-ECS. Généralement, le scénario AWS-ECS contient six opérations principales : 1- ItemSearc h : rechercher, en utilisant un mot clé, dans la base de données d’Amazon les articles rapprochés et renvoie une liste de produits correspondant aux critères de recherche. 2- CartCreat e : prend en entrée un ASIN (un identificateur unique pour un élément dans la base de données d’Amazon) et un entier ‘ n ‘ positif, et crée un nouveau panier d’achats qui représente une demande de n copies de cet élément. Amazon stocke et gère le contenu du panier. Les opérations SOAP réfèrent au panier en passant son identifiant unique. 3- Cart Clea r : vide le panier avec un ID donné. 4- Cart Add : ajoute une nouvelle ligne à un panier donné demandant n copies de certains AS IN. 5- Cart Remove : supprimer tous les articles d’un panier donné. 6- Cart Edi t : modifie la quantité d’un certain article dans un panier donné .

LLRP

La radio-identification ou RFID (Radio Frequency Identification) est une technologie sans fil qui permet de mémoriser et de récupérer des données à distance en utilisant des marqueurs appelés « radioétiquettes » (ou « RFID tag »). Les tags RFID sont des balises métalliques qui peuvent être collées ou incorporées dans des produits et qui sont composées d’une antenne et d’une puce électronique, qui réagissent aux ondes radio et qui transmettent des informations à distance. Un système de radio-identification se compose de deux entités : les tags RFID et un ou plusieurs lecteurs. Les lecteurs sont des dispositifs, émetteurs de radiofréquences qui vont activer les tags. La configuration des lecteurs RFID se fait via un protocole qui s’appelle LLRP (Low Level Reader Protocol) (EPC-Globel, 2007). Il fournit des moyens de contrôler les aspects du fonctionnement des tags, y compris les paramètres de protocole et les paramètres d’individualisation.

Une séquence typique LLRP entre le client et le lecteur RFID suit le processus suivant :
1- Vérification des capacités du lecteur par le client
2- Réglage de la configuration du client .
3- Envoi des commandes des configurations du lecteur. Ces commandes sont appelées spécifications de fonctionnement du lecteur (ROSpecs : Reader Operation Specifications). Elles contiennent une liste de commandes séquentielles des opérations d’inventaire appelé AISpec (Antenna Inventory Specifications)
4- Envoyer les spécifications d’accès du lecteur (AccessSpec)
5- Obtenir le rapport du lecteur .

Les événements dans ce scénario sont les états des transitions d’un ROSpec. La Figure 2.3 illustre les états des transitions d’un ROSpec. Le ROSpec possède trois états : « Disabled », « Active » et « Inactive ». Le client configure une nouvelle ROSpec en utilisant le message ADD_ROSPEC pour le ROSpec. Le ROSpec commence à l’état « Disabled » en attendant le message « ENABLE_ROSPEC » pour le ROSpec du client sur lequel il passe à l’état « Inactive ». À l’état « Disabled », le ROSpec ne répond pas aux demandes d’arrêt ou de démarrage des déclencheurs. Le client désactive un ROSpec grâce au message « DISABLE_ROSPEC » pour le ROSpec. Les transitions de l’état « Inactive » à l’état « Active » de ROSpec surviennent lorsqu’un message « ROSpecStartConditio n » arrive pour le ROSpec. Les transitions ROSpec reviennent à l’état « Inactive » lorsqu’un message « ROSpecDoneCondition » arrive. Lorsque le ROSpec est indéfini, il n’est plus considéré pour l’exécution. Le client annule le ROSpec avec le message « DELETE_ROSPEC ».

CONCLUSION

Ce projet de recherche apporte des solutions à la problématique énoncée en introduction qui porte sur l’analyse des traces d’événements. L’analyse des traces d’événements permet d’identifier des erreurs dans l’exécution du système ou la violation de certaines politiques. Le principe de cette analyse consiste à vérifier si un système respecte un contrat donné. Plusieurs outils ont été développés pour résoudre ce problème. Ces outils sont mal documentés en ce qui a trait à leur performance. De plus, la plupart des solutions existantes ont été développées pour une utilisation particulière. Aussi, dans la plupart des scénarios, le temps et la mémoire consommée varient beaucoup d’un scénario à l’autre sans qu’il existe un consensus à savoir quelle méthode fonctionne le mieux.

Table des matières

CHAPITRE 1 INTRODUCTION
1.1 Exemples
1.2 Problématique et objectif
1.3 Méthodologie
1.4 Contexte de la recherche
1.5 Organisation du document
CHAPITRE 2 SCÉNARIOS DE VÉRIFICATION DES TRACES
2.1 Bookstore
2.2 Amazon E-Commerce web service
2.3 LLRP
2.4 Cycle générateur
2.5 Nombres aléatoires
CHAPITRE 3 FORMALISATION
3.1 Modèle de base: XML
3.2 Un modèle formel des traces d’événements
3.2.1 Trace multi valeurs
3.2.2 Trace à une seule valeur
3.2.3 Trace à un schéma fixe
3.2.4 Trace atomique
3.3 Propriétés sur les traces d’événements
3.3.1 Les automates
3.3.2 Les expressions régulières
3.3.3 LTL
3.3.4 LTL-FO+
3.3.5 MFOTL
CHAPITRE 4 OUTILS D’ANALYSE DES TRACES D’ÉVÉNEMENTS
4.1 Analyse des logs
4.1.1 Maude
4.1.2 Saxon
4.1.3 MySQL
4.2 Model checking
4.2.1 NuSMV
4.2.2 SPIN/Promela
4.2.3 Autres outils
4.3 Vérification au moment de l’exécution (runtime monitoring)
• 4.3.1 BeepBeep
4.3.2 Monpoly
4.3.3 Autres outils
CHAPITRE 5 EXPÉRIMENTATION
5.1 Implementation
5.2 Les générateurs des traces
5.2.1 Amazon
5.2.2 Bookstore
5.2.3 Cycle Generator
5.2.4 LLRP generator
5.2.5 Random generator
5.3 Traductions et transductions
5.3.1 Transduction de LTL à des atomes
5.3.2 Traduction de NuSMV
5.3.3 Traduction de SPIN
5.3.4 Transduction de LTL à SQL
5.3.5 Transduction de LTL-FO+à XQuery
5.4 Résultats et discussion
5.5 Démarches pour obtenir les outils
CHAPITRE 6 CONCLUSION

Télécharger le rapport complet