Search

There is a strong link between software quality and software reliability. By decreasing the probability of imperfection in the software, we can augment its reliability guarantees. At one extreme, software with one unknown bug is not reliable. At the other extreme, perfect software is fully reliable. Formal verification with SPARK has been used for years to get as close as possible to zero-defect software. We present the well-established processes surrounding the use of SPARK at Altran UK, as well as the deployment experiments performed at Thales to finetune the gradual insertion of formal verification techniques in existing processes. Experience of both long-term and new users helped us define adoption and usage guidelines for SPARK based on five levels of increasing assurance that map well with industrial needs in practice., Electronic Communications of the EASST, Volume 76: Automated Verification of Critical Systems 2018 (AVoCS 2018)

We are interested in the problem of providing safe and secure software for drones to make themas safe as airplanes. As there is no certification standard for most commercial drones that exist today, wehave chosen the well-known DO-178C/ED-12C avionics standard as a framework to define a suitable formaldevelopment and verification process. Our process is based on this standard and its three supplements: DO-331/ED-218 (model based development), DO-332/ED-217 (object oriented technology) and DO-333/ED-216(formal methods). Our process is an original adaptation of the usual V-cycle based avionics processes to aniterative and incremental environment, where development and verification are performed in shortincrements. In this paper, we describe how we achieve that in practice and discuss in more details theintegration of the formal methods supplement.

The value of lightweight checkers, aka linters, for finding bugs in C or C++ programshas long been recognized. Their value for strongly typed languages like Ada or OCaml has notbeen so evident, as the compiler for these languages typically rules out most classes of bugsthat C/C++ linters find, either by issuing errors for non-compliance with language rules, or moreprecise warnings thanks to the additional information available to the compiler. In particular, theavailability of deep static analysis tools for these languages makes it uncertain that linters canbe of interest too, as the power of their analysis fits between compilers and deep static analysistools. We have investigated this question for the language Ada, and we have found that linterscan play an important role for such languages as well, which is more focused than the role theytraditionally play for weaker languages. Our findings are based on the creation of a set of lintersfor Ada that we applied to multiple industrial active codebases that we maintain at AdaCore. Theresults of these experiments were eye opening on the value of linters for stronger languages. Inthis article, we also describe the technology that allows the easy development and deploymentof​ ​ linters,​ ​ as​ ​ well​ ​ as​ ​ our​ ​ strategy​ ​ for​ ​ adapting​ ​ linters​ ​ to​ ​ the​ ​ analysis​ ​ context.

In critical software systems like the ones related to transport and defense, it is common toperform numerical computations implemented using floating-point arithmetic. Safety conditions for suchsystems typically require strong guarantees on the functional behavior of the performed computations.Automatically verifying that these guarantees are fulfilled is thus desirable.Deductive program verification is a promising approach for verifying that a given code fulfills a functionalspecification, with a very high level of confidence. Yet, formally proving correct a program performingfloating-point computations remains a challenge, because floating-point arithmetic is not easily handled byautomated theorem provers.We address this challenge by combining multiple techniques to separately prove parts of the desired proper-ties. On the one hand, abstract interpretation computes numerical bounds for expressions that appear eitherin the original program, or in the ghost code added to instrument the program. On the other hand, we gen-erate verification conditions for different automated provers, relying on different strategies for representingfloating-point computations. Among these strategies, we try to exploit the native support for floating-pointarithmetic recently added in the SMT-LIB standard.Our approach is partly implemented in the Why3 environment for deductive program verification, and partlyimplemented in its front-end environment SPARK for the development of safety-critical Ada programs. Wereport on several examples and case studies used to validate our approach experimentally.; Dans les logiciels critiques comme ceux liés aux transports et à la défense, il est courant d’effectuer des calculs numériques implémentés à l’aide de l’arithmétique à virgule flottante. Les exigences de sûreté de ces systèmes requièrent généralement des garanties fortes sur le comportement fonctionneldes calculs ainsi exécutés. Vérifier automatiquement que ces garanties sont remplies est donc souhaitable.La vérification déductive des programmes est une approche prometteuse pour vérifier formellementqu’un code donné satisfait une spécification fonctionnelle, avec un haut niveau de confiance. Néanmoins, prouver formellement qu’un programme qui effectue des calculs en virgule flottante est correct reste un défi, car l’arithmétique à virgule flottante n’est pas facilement traitée par les prouveurs automatiques.Nous abordons ce défi en combinant plusieurs techniques pour prouver séparément chaque partie despropriétés souhaitées. D’une part, l’interprétation abstraite calcule les bornes numériques pour les expressions qui apparaissent dans le programme d’origine, ou dans le code fantôme ajouté pour instrumenter le code. D’autre part, nous générons des obligations de preuve pour plusieurs prouveurs automatiques différents, s’appuyant sur différentes représentations des calculs en virgule flottante. En particulier, nous exploitons le support natif de l’arithmétique en virgule flottante récemment apparue dans le standard SMT-LIB.Notre approche est mise en oeuvre en partie dans la boîte à outils générique Why3 pour la vérificationdéductive, et en partie dans l’environnement SPARK pour le développement de programmes Ada critiques. Nous présentons des exemples et études de cas qui ont été utilisées pour valider notre approche expérimentalement.

In critical software systems like the ones related to transport and defense, it is common toperform numerical computations implemented using floating-point arithmetic. Safety conditions for suchsystems typically require strong guarantees on the functional behavior of the performed computations.Automatically verifying that these guarantees are fulfilled is thus desirable.Deductive program verification is a promising approach for verifying that a given code fulfills a functionalspecification, with a very high level of confidence. Yet, formally proving correct a program performingfloating-point computations remains a challenge, because floating-point arithmetic is not easily handled byautomated theorem provers.We address this challenge by combining multiple techniques to separately prove parts of the desired proper-ties. On the one hand, abstract interpretation computes numerical bounds for expressions that appear eitherin the original program, or in the ghost code added to instrument the program. On the other hand, we gen-erate verification conditions for different automated provers, relying on different strategies for representingfloating-point computations. Among these strategies, we try to exploit the native support for floating-pointarithmetic recently added in the SMT-LIB standard.Our approach is partly implemented in the Why3 environment for deductive program verification, and partlyimplemented in its front-end environment SPARK for the development of safety-critical Ada programs. Wereport on several examples and case studies used to validate our approach experimentally.; Dans les logiciels critiques comme ceux liés aux transports et à la défense, il est courant d’effectuer des calculs numériques implémentés à l’aide de l’arithmétique à virgule flottante. Les exigences de sûreté de ces systèmes requièrent généralement des garanties fortes sur le comportement fonctionneldes calculs ainsi exécutés. Vérifier automatiquement que ces garanties sont remplies est donc souhaitable.La vérification déductive des programmes est une approche prometteuse pour vérifier formellementqu’un code donné satisfait une spécification fonctionnelle, avec un haut niveau de confiance. Néanmoins, prouver formellement qu’un programme qui effectue des calculs en virgule flottante est correct reste un défi, car l’arithmétique à virgule flottante n’est pas facilement traitée par les prouveurs automatiques.Nous abordons ce défi en combinant plusieurs techniques pour prouver séparément chaque partie despropriétés souhaitées. D’une part, l’interprétation abstraite calcule les bornes numériques pour les expressions qui apparaissent dans le programme d’origine, ou dans le code fantôme ajouté pour instrumenter le code. D’autre part, nous générons des obligations de preuve pour plusieurs prouveurs automatiques différents, s’appuyant sur différentes représentations des calculs en virgule flottante. En particulier, nous exploitons le support natif de l’arithmétique en virgule flottante récemment apparue dans le standard SMT-LIB.Notre approche est mise en oeuvre en partie dans la boîte à outils générique Why3 pour la vérificationdéductive, et en partie dans l’environnement SPARK pour le développement de programmes Ada critiques. Nous présentons des exemples et études de cas qui ont été utilisées pour valider notre approche expérimentalement.

A major issue in the activity of deductive program verification is the understanding of the reason for why some proof fails. To help the user understand the problem and decide what needs to be fixed in the code or the specification of her program, it is essential to provide means to investigate such a failure. To that mean, we propose a technique for generatingcounterexamples, exhibiting some values for the variables of the program where a given part of the specification fails to be validated. To produce such a counterexample, we exploit the ability of SMT (Satisfiability Modulo Theories) solvers to propose, when a proof of a formula is not found, a counter-model. Turning such a counter-model into a counterexample for the initial program is not a trivial task because of the many transformations that lead from a given code and specification to a verification condition. We report on our approach for the design and the implementation of counterexample generation within the SPARK 2014 environment for the development of safety-critical Ada programs; Un défi important de l’activité de vérification déductive de programmes est la compréhension de la raison pour laquelle une certaine preuve échoue. Pour aider l’utilisateur à comprendre le problème et à décider quoi modifier dans son code ou bien sa spécification, il est essentiel de fournir des moyens d’analyser l’échec de preuve. À cette fin, nous proposons une technique de génération de contre-exemples, qui exhibent des valeurs pour les variables du programme pour lesquelles une certaine partie de la spécification ne peut pas être prouvée. Pour produire un tel contre-exemple, nous exploitons la capacité des solveurs SMT (Satisfiability Modulo Theories) de proposer, quand une formule n’est pas prouvée, un contre-modèle. Transformer un tel contre-modèle en un contre-exemple pour le programme de départ n’est pas une tâche facile à cause des multiples transformations qui conduisent du code et de la spécification de départ vers une obligation de preuve. Nous présentons l’approche que nous avons suivie pour la conception et l’implémentation de la génération de contre-exemples dans le cadre de l’environnement SPARK 2014 pour le développement de programmes Ada critiques

A major issue in the activity of deductive program verification is the understanding of the reason for why some proof fails. To help the user understand the problem and decide what needs to be fixed in the code or the specification of her program, it is essential to provide means to investigate such a failure. To that mean, we propose a technique for generatingcounterexamples, exhibiting some values for the variables of the program where a given part of the specification fails to be validated. To produce such a counterexample, we exploit the ability of SMT (Satisfiability Modulo Theories) solvers to propose, when a proof of a formula is not found, a counter-model. Turning such a counter-model into a counterexample for the initial program is not a trivial task because of the many transformations that lead from a given code and specification to a verification condition. We report on our approach for the design and the implementation of counterexample generation within the SPARK 2014 environment for the development of safety-critical Ada programs; Un défi important de l’activité de vérification déductive de programmes est la compréhension de la raison pour laquelle une certaine preuve échoue. Pour aider l’utilisateur à comprendre le problème et à décider quoi modifier dans son code ou bien sa spécification, il est essentiel de fournir des moyens d’analyser l’échec de preuve. À cette fin, nous proposons une technique de génération de contre-exemples, qui exhibent des valeurs pour les variables du programme pour lesquelles une certaine partie de la spécification ne peut pas être prouvée. Pour produire un tel contre-exemple, nous exploitons la capacité des solveurs SMT (Satisfiability Modulo Theories) de proposer, quand une formule n’est pas prouvée, un contre-modèle. Transformer un tel contre-modèle en un contre-exemple pour le programme de départ n’est pas une tâche facile à cause des multiples transformations qui conduisent du code et de la spécification de départ vers une obligation de preuve. Nous présentons l’approche que nous avons suivie pour la conception et l’implémentation de la génération de contre-exemples dans le cadre de l’environnement SPARK 2014 pour le développement de programmes Ada critiques

It is widely acknowledged that the main source of cost for developing high-integrity software systems is their verification. A significant portion of this verification cost is spent assessing that software complies with its requirements. Over the years several different methods have been developed to address this issue, in particular: testing, peer reviews, formal verification and automatic code generation. It is more and more frequent that these verification strategies are mixed within the same system, so as to adopt the most appropriate one for each component. This increases the complexity of the integration phase because it has to cope with multiple formalisms, development and verification methods. Our goal is to propose a pragmatic process to integrate components developed using different methods into a single system and demonstrate that properties already verified for each component in isolation are preserved in their composition. This process leverages AADL as a pivotal modeling language for system specification and relies on specific verifications between the latter and the components developed using heterogeneous modeling and programming languages, namely Simulink for computation intensive parts and Ada/SPARK 2014 for other components. Our paper proceeds as follows. First we provide a high-level overview of our approach and enumerate the current methods for addressing the property preservation problem. Then we illustrate practically our approach using the Nose Gear Challenge problem, a simplified yet complete example of a high-integrity real-time system. We then conclude by comparing our approach to the state of the art.