Vérification parallélisée de propriétés temporelles sur des traces d'exécution, par analyse dynamique formelle
FERLIN ; BON ; WIELS ; COLLART-DUTILLEUL
Type de document
COMMUNICATION AVEC ACTES INTERNATIONAL (ACTI)
Langue
francais
Auteur
FERLIN ; BON ; WIELS ; COLLART-DUTILLEUL
Résumé / Abstract
Les méthodes de vérification peuvent être classées suivant deux critères : une méthode peut être statique ou dynamique, ainsi que formelle ou informelle. Ce papier poursuit des travaux de thèse sur la vérification de propriétés temporelles sur des traces d'exécution par analyse dynamique formelle. L'approche proposée consiste à transformer une propriété LTL en automate de Büchi et à exécuter ce dernier sur une trace pour l'analyser. Le problème de fin de trace lié à l'utilisation de LTL sur des traces finies peut être contourné par le calcul d'informations statistiques à condition que la propriété suive un patron prédéfini. Pour des traces de très grande taille, cette approche est bien adaptée, mais nécessite que la trace soit vérifiée séquentiellement. Cet article propose de remédier à ce problème, en découpant la trace en plusieurs sous-traces analysables séparément, suivant une stratégie définie, ce qui permet un gain de temps significatif.
