Revue de la vérification de l’exécution et des travaux connexes 

VÉRIFICATION DE L’EXÉCUTION 

La vérification et la validation de logiciels, étant considéré comme un aspect important de la gestion de projet et de l’ingénierie du logiciel, est le processus pour utiliser diverses techniques nécessaires pour détecter les violations ou les satisfactions et d’évaluer la qualité des logiciels et la performance d’un système (IEEE, 2012).

CONCEPTS FONDAMENTAUX
Il y a normalement deux types de techniques de vérification : analyse statique et dynamique. Certains techniques traditionnelles bien connues d’analyse statique sont la vérification de modèles (Clarke et al., 1999) et la démonstration de théorèmes (Heisel et al., 1990). L’analyse statique est généralement appliquée pour vérifier les comportements d’un système avant son exécution, mais ces techniques ont des lacunes naturelles. Par exemple, la vérification de modèles ne peut pas fonctionner sur un système dont la taille ou le nombre d’états pourraient se développer au-delà de la capacité de puissance de calcul en raison de la “state-explosion problem”.

L’analyse dynamique est destinée de surveiller les systèmes en cours d’exécution. Bien que parfois le résultat pourrait être de faux négatifs à cause de son incomplétude, celle-ci permet aux techniques d’analyse dynamique de briser la limitation de méthodes statiques et devenir ainsi les méthodes complémentaires de vérification. (Falcone et al., 2013) .

la vérification de l’exécution est une sorte de technique de vérification sur la base de l’analyse dynamique. En 2001, le Runtime Verification workshop  a été fondée, comme la terminologie “runtime verification” qui a été officiellement établie (Wikipedia, 2016). Elle est une technique relativement nouvelle qui est légère et qui vise à compléter d’autres techniques traditionnelles de vérification comme “model checking” et “testing”.

Leucker et Schallhart (2009) définissent la vérification de l’exécution comme suit :

“Runtime verification is the discipline of computer science that deals with the study, development, and application of those verification techniques that allow checking whether a run of a system under scrutiny satisfies or violates a given correctness property.”

Normalement, lorsqu’une violation est observée, la vérification de l’exécution ne résout pas le programme détecté en soi, mais son résultat est un guide et une base importante pour d’autre composants dans le même système pour régler le problème.

Leucker et Schallhart (2009) définissent également un run d’un système en tant qu’une séquence de traces infinies du système, et une exécution d’un système comme une trace finie et aussi un préfixe fini d’un run. Le travail de la vérification de l’exécution se concentre principalement sur l’analyse d’exécutions qui sont effectuées par les moniteurs.

Un moniteur est une procédure de décision générée (ou “synthétisée”) à partir de l’une des propriétés formelles qui doit être vérifiée par rapport à l’exécution du système donné. Lors de la vérification, un moniteur énumère les traces finies d’un exécution, vérifie si elles satisfont aux propriétés d’exactitude et produit un verdict comme le résultat. Un verdict, qui est normalement une valeur de vérité, indique la satisfaction de la propriété par rapport aux événements recueillis.

Un verdict dans la plupart des cas simples peut être normalement exprimé comme vrai/faux, oui / non ou 1/0, selon le contexte. Mais en réalité, de nombreux systèmes de la vérification de l’exécution doivent introduire d’autres valeurs pour fournir un résultat plus précis. Par exemple, grâce à l’incomplétude du système de la vérification de l’exécution, un verdict ne peut pas être facilement émis lorsque le moniteur a besoin de plus d’événements successifs, donc une valeur inconcluante (écrite comme “ ?”) est introduite pour indiquer l’état présent du système surveillé. (Falcone et al., 2013) .