Remember Me
Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:

OpenAIRE is about to release its new face with lots of new content and services.
During September, you may notice downtime in services, while some functionalities (e.g. user registration, login, validation, claiming) will be temporarily disabled.
We apologize for the inconvenience, please stay tuned!
For further information please contact helpdesk[at]openaire.eu

fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Champion, Adrien (2014)
Languages: English
Types: Article
Subjects: 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

Cite this article

Cookies make it easier for us to provide you with our services. With the usage of our services you permit us to use cookies.
More information Ok