Analyse de logs guidée par des vérifications de formules de responsabilité exprimées en CTL
Résumé
Ce document présente une méthode de modélisation d’un ensemble de logs par une structure de Kripke, permettant ainsi son interrogation en utilisant la logique temporelle CTL. Nous prendrons comme exemple une série de logs fournis par l’équipe Amazones de l’Insa de Lyon, que nous modéliserons suivant l’approche proposée. Nous proposons la spécification de quelques propriétés de responsabilité et nous détaillerons l’état actuel du prototype développé.