Building Confidence on Formal Verification Models

Abstract : A problem hindering the adoption of formal methods in the industry is how to integrate the models and results used during formal verification with existing processes. Indeed, formal verification is a complex process involving multiple methods, models, level of formality, ... If we want to use formal verification results in an assurance case, it is therefore necessary to build confidence on this process. The integration of formal methods raises particular problems like, for instance, with the construction of the verification models: a model may not preserve all properties of the system to be verified; it may only cover a subset of these properties; or it may be intractable. In practice, this means that the verification process involves a collection of models whose soundness (with the original system design, but also between each others) shall be justified. Furthermore, formal techniques are usually restricted in terms of the set of properties that can be checked. It is therefore necessary to justify (and trace back) that these restrictions are consistent with the hypotheses made about the system, its application and its environment. This short abstract gives an overview of a methodology for building verification arguments, that is convincing arguments that a system design complies with a set of properties.
Type de document :
Communication dans un congrès
Fast Abstracts at International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Sep 2016, Trondheim, Norway. 2016
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.laas.fr/hal-01369144
Contributeur : Jérémie Guiochet <>
Soumis le : mercredi 21 septembre 2016 - 14:27:20
Dernière modification le : vendredi 26 octobre 2018 - 10:34:53
Document(s) archivé(s) le : jeudi 22 décembre 2016 - 12:20:17

Fichier

2-bourdil-jenn-dalzilio.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01369144, version 1

Citation

Pierre-Alain Bourdil, Eric Jenn, Silvano Dal Zilio. Building Confidence on Formal Verification Models. Fast Abstracts at International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Sep 2016, Trondheim, Norway. 2016. 〈hal-01369144〉

Partager

Métriques

Consultations de la notice

256

Téléchargements de fichiers

127