Collaboration de techniques formelles pour la vérification de propriétés de sûreté sur des systèmes de transition

Other literature type English OPEN
Champion, Adrien (2014)
  • Subject: Smt | Sat | K-induction | Interprétation abstraite | Élimination de quantificateurs | Méthodes formelles | 621.39 | Abstract interpretation | Quandtifier elimination | Formal methods

Ce travail porte sur la vérification de composants logiciels dans les systèmes embarqués critiques avioniques. Les conséquences d’une erreur dans de tels systèmes pouvant s'avérer catastrophiques, il se doivent de respecter leur spécification. La vérification formelle tend à prouver cette adéquation si elle est vraie, ou à produire un contre-exemple si elle ne l’est pas. Les méthodes actuelles ne sont pas capable de traiter les les systèmes industriels. La découverte d’informations supplémentaires (invariants) sur le système permet de réduire l’espace de recherche afin de renforcer l’objectif de preuve: les informations découvertes sont suffisantes pour conclure “facilement”. Nous définissons une architecture parallèle permettant à des méthodes de découverte d’invariants de collaborer autour d’un moteur de kinduction. Dans ce contexte nous proposons HullQe, une nouvelle heuristique de génération d’invariants potentiels combinant un calcul de pré-image par élimination de quantificateurs et des calculs d’enveloppes convexes. Nous montrons que HullQe est capable, automatiquement, de renforcer des objectifs de preuve correspondant à la vérification de patrons de conception courants en avionique. Pour autant que nous sachions, les méthodes actuelles sont incapables de conclure sur ces problèmes. Nous détaillons nos améliorations de l’algorithme d’élimination de quantificateurs de Monniaux afin d’assurer le passage à l’échelle sur nos systèmes. Notre framework formel Stuff est une implémentation de notre architecture parallèle composée de HullQe, d'une technique de découverte d’invariants basée sur des templates, et d'une généralisation de PDR à l’arithmétique. This work studies the verification of software components in avionics critical embedded systems. As the failure of such systems can have catastrophic consequences, it is mandatory to make sure they are consistent with their specification. Formal verification consists in proving that a system respects its specification if it does, or to produce a counterexample if it does not. Current methods are unable to handle the verification problems stemming from realistic systems. Discovering additional information (invariants) on the system can however restrict the search space enough to strengthen the proof objective: the information discovered allow to "easily" reach a conclusion. We define a parallel architecture for invariant discovery methods allowing them to collaborate around a k-induction engine. In this context we propose a new heuristic for the generation of potential invariants by combining an iterated preimage calculus by quantifier elimination with convex hull computations, called HullQe. We show that HullQe is able to automatically strengthen proof objectives corresponding to safety properties on widespread design patterns in our field. To the best of our knowledge, these systems elude current techniques. We also detail our improvements to the quantifier elimination algorithm by David Monniaux in 2008, so that it scales to computing preimages on our systems. Our formal framework Stuff is an implementation of the parallel architecture we propose in which we implemented not only HullQe, but also a template-based invariant discovery technique, and a generalisation to Property Directed Reachability to linear real arithmetic and integer octagons.
Share - Bookmark