Technique de programmation par contraintes pour la vérification bornée des programmes : une stratégie non-séquentielle appliquée à un système embarqué critique
Institution:
NiceDisciplines:
Directors:
Abstract EN:
This thesis is devoted to program verification using the constraint programming technique. In particular, it focus on the incremental exploration strategy of executable paths of a program for verification and automatic counterexample generation using constraint solvers such as CP, LP, MIP, SMT. The context of this work is the Bounded Model Checking (BMC), an incomplete formal verification method, which only deals with paths of a bounded length in programs. In this thesis, we propose DPVS (Dynamic Postcondition-Variables driven Strategies), a new strategy based on the dynamic generation of a system of constraints in during the exploration of the control flow graph of the program. DPVS uses a backward search technique guided by the variables related to the property to prove. This strategy was evaluated on academic examples and real applications. Experiments on an industrial controller which manages the flashing lights of a car show that our system is more efficient than CPBPV, our previous approach, and than CBMC, a-state-of-the-art bounded model checker. We have developed a prototype in COMET that uses the DPVS strategy for program verification and automatic generation of counterexamples. This prototype uses many classical techniques to simplify the control flow graph such as calculating bounds of variables, slicing, propagation of constants. DPVS was successful in finding a counter–example of a real application, the Flasher Manager, that was provided by Gensoft, an industrial partner of the research project TESTEC.
Abstract FR:
Cette thèse porte sur la vérification bornée des programmes à l’aide de la technique de programmation par contraintes. Plus précisément, sur la stratégie d’exploration incrémentale des chemins exécutables pour la vérification et pour la génération automatique de contre-exemples d’applications. Cela est fait en utilisant les solveurs de contraintes comme les solveurs CP, LP, MIP, SMT. Nous avons utilisé dans ces travaux les méthodes de vérification formelles incomplètes ou Bounded Model Checking (BMC). Ces méthodes traitent uniquement des chemins d’une taille bornée dans les programmes. Dans cette thèse, nous proposons DPVS (Dynamic Postcondition-Variables driven Strategies), une nouvelle stratégie basée sur la génération dynamique d’un système de contraintes lors de l’exploration du graphe de flot de contrôle d’un programme. DPVS utilise une technique de recherche ascendante guidée par les variables liées à la propriété à prouver. Cette stratégie a été évaluée sur des exemples académiques et sur des applications réelles. Les expérimentations sur un contrôleur industriel qui gère les clignotants d’une voiture ont montré que notre système est bien plus performant que CPBPV (une approche proposée au sein de notre équipe) ainsi qu’un outil de model checking de premier plan comme CBMC. Nous avons également développé un prototype en COMET qui utilise la stratégie DPVS pour la vérification de programmes et pour la génération automatique des contre-exemples. Ce prototype utilise plusieurs techniques classiques pour simplifier le graphe de flot de contrôle : calcul de bornes de variables, technique de slicing, technique de propagation de constantes. Grâce à DPVS, nous avons trouvé des contre-exemples pour l’application temps-réel Gestionnaire des clignotants qui est fournie par Gensoft, un partenaire industriel du projet de recherche TESTEC.