Software Verification
2023-2024
TP3: Bounded Model Checking

Vincent Penelle

Points abordés



Le but de ce TP consiste à vous faire programmer deux modules DepthFirstBMC.ml et GlobalBMC.ml de notre outil Simple Program Analyser. Ces module implémenteront chacun un algorithme de Bounded Model Checking explorant l’arbre d’exécution, le premier en profondeur, le second niveau par niveau grâce au dépliage de la formule de pas.

Rappel:

Un control-flow automaton est un tuple (Q,qi,qbad,Δ) où Q est un ensemble fini d’états, qiQ est l’état initial, qbad est l’état terminal (ou «mauvais»), et Δ ⊆ Q × Op × Q est l’ensemble des transitions, où Op est l’ensemble des opérations possibles de l’automate. Cet ensemble est défini ci-après. Autrement dit, c’est un automate étiqueté par des opérations (sur des variables).

On considère un ensemble de variables X. Une opération peut être soit skip, une garde ou une affectation de la forme x := exp, pour xX et exp une expression arithmétique:

op ::= skip | guard | x := exp

(cf TP précédent pour plus de détails sur les opérations et leur sémantique)

Point technique:

Une configuration d’un control-flow automaton A est un couple (q,σ), où q est un état, et σ est une fonction de X dans ℤ appelée valuation.

La sémantique d’une opération op est la relation [| op |] qui contient les valuations (σ12) telles que σ2 peut être obtenue en appliquant op à σ1. Formellement, on a [| skip |] = id, [| guard |] est l’ensemble des (σ,σ) tels que σ satisfait la garde, et [| x := exp |] = {(σ,σ[x:=exp])}. Cf TP précédent pour plus de détails et l’implémentation en formule de SMT.

La sémantique d’une transition t = (q,op,q′) est la relation binaire →t sur les configurations définie par ct c′ si c = (q,σ), c′ = (q′,σ′) et (σ,σ′) ∈ [| op |].

La step relation (ou relation de pas) →A est l’union de toutes les sémantiques des transitions de A .

Une éxecution est une séquence c0, t1, c1, …, tn, cn alternant configurations ci et transitions ti telles que ci−1ti ci pour tout 0 < in. Une telle éxecution est également écrite c0t1 c1 ⋯ →tn cn pour améliorer la lisibilité, et n est sa longueur.

Un chemin q0, op1, q1, …, opn, qn est dit éxécutable si il existe des valuations ρ0, …, ρn ∈ ℤX telles que (q0, ρ0) →t1 (q1, ρ1) ⋯ →tn (qn, ρn) soit une éxecution, avec ti = (qi−1, opi, qi).

Point technique:

Le problème du bounded model-checking demande, étant donné un control-flow automaton A et une borne k ∈ ℕ, s’il existe deux configurations (q,ρ) et (q′,ρ′) telles que:

Le problème peut être formulé de manière équivalente ainsi : Existe-t’il un chemin éxécutable de longueur au plus k de qi à qbad.

L’algorithme du bounded model-checking peut être simplement résumé ainsi: énumérer toutes les chemins de longueur au plus k, et dès qu’on en trouve un éxécutable de l’état initial à l’état cible, renvoyer ce chemin.

Bien évidemment, il existe plusieurs ordres d’explorations possible de ces chemins, et quelques optimisations simples, mais efficaces (notamment, il ne sert à rien de regarder un chemin si on sait que l’un de ses préfixes n’est pas éxécutable). On peut également demander au programme de déterminer si il a effectué une exploration exhaustive ou non (s’il existait des éxécutions plus longues que celles regardée ou non).

Ici, nous allons implémenter un ordre d’exploration en profondeur des chemins : cela consiste, étant donné un ordre (arbitraire) sur les transitions, regarder d’abord tous les chemins commençant par la première, puis ceux commençant par la seconde, etc. Dès que l’on atteint la borne où un chemin non-exécutable, on remonte au niveau supérieur et on continue l’exploration à partir de là. Dès qu’on atteint un mauvais chemin éxécutable, on stoppe l’exploration et on le renvoie.

Plus précisément, l’algorithme (récursif), reçoit en entrée, un CFA A, un chemin τ, un état courant q, la profondeur courante ℓ, et la borne k, et peut être résumé comme suit :

L’algorithme est appelé sur (A,(qi),qi,0,k) pour effectuer le bounded model-checking avec borne k sur l’automate A.

Exercice 1: Depth-first search bounded model-checking

Téléchargez l’archive du TP. Dans le fichier DepthFirstBMC.ml, vous avez à coder la fonction dfs qui réalise le parcours en profondeur de l’arbre décrit ci-dessus. Le commentaire au dessus du prototype la fonction contient tout ce qu’il faut pour vous aider à programmer cette algorithme, notamment en adaptant les arguments pour faciliter le travail du programme (en retenant une formule décrivant le chemin jusqu’ici plutôt que le chemin lui-même, par exemple). Il y aura quelques subtilités qui vous sont laissées pour renvoyer correctement le chemin fautif.

Vous pouvez également tester votre programme sur les exemples fournis, et comparer avec l’exécutable fonctionnel vous étant fourni bmc.solution.d.byte.

Point technique:

L’algorithme global consiste à déterminer, longueur par longueur jusqu’à la borne, s’il existe un chemin de cette longueur. Cela revient à se demander, pour une longueur k, s’il existe des états q1,⋯,qk−1 de l’automates et des valuations X0,⋯,Xk, tels que (qin,X0A (q1,X1) →A ⋯ →A (qk−1,Xk−1) →A (qbad,Xk).

Pour cela, on commence par calculer la formule φstep de l’automate, reliant deux configurations si et seulement si l’automate permet de passer de l’une à l’autre. Avec cette formule, pour chaque profondeur i jusqu’à la borne, on vérifie si la formule suivante est satisfaisable ou non :

  ψi(q0,X0,⋯,qi,Xi)  
def
=
 
    q0 = qin ∧ 
i
j = 1
 ϕstep(qj−1, Xj−1, qj, Xj) ∧ qi = qbad

Si elle l’est, on a l’existence d’un éxécution de bug (et il faut le reconstruire grâce au modèle de la formule (sachant qu’il manque des informations pour récupérer les transitions dans la formule donnée ici)). Si elle ne l’est pas, il n’y a aucun éxécution de bug à la profondeur i. Si on a fait les profondeurs une à une, on peut donc passer à la suivante.

À noter que évidemment, il ne sert à rien de tester ψi si aucune éxécution de longueur i n’existe. Pour le déterminer, il suffit de demander au solveur de tester ψi sans assurer que le dernier état est qbad (c-à-d sans la partie rouge). Si oui, on doit continuer l’exploration, mais si elle est insatisfiable, il n’y a aucune éxécution de longueur i, et donc on peut dire que le programme est correcte (recherche exhaustive).

Exercice 2: Global bounded model-checking

Dans le fichier GlobalBMC.ml, implémentez les fonctions indiquées. Des indications y sont données. N’hésitez pas à découper votre code avec des fonctions auxiliaires. Dans Z3Helper.mli, vous avez des fonctions pour vous aider à manipuler les états et transitions de l’automate dans la formule.

Commencez par implémenter une version sans vous préoccuper de renvoyer le contre-exemple trouvé, puis modifiez la formule pour pour renvoyer ce contre-exemple.


Ce document a été traduit de LATEX par HEVEA