Category Archives: Open-DO News

DO-330/ED-215 Benefits of the New Tool Qualification Document

By Jamie Ayre | January 25, 2013

As part of the DO-178C/ED-12C revision effort, a new document Software Tools Qualification Considerations (DO-330/ED-215) was developed. Its goal is both to replace the software tool qualification guidance of DO-178B/ED-12B and also to enable and encourage the use of this “mature” guidance outside the airborne domain. Since it may be used independently, DO-330/ED-215 is not considered as a supplement to DO-178C/ED-12C; it is thus titled differently from the specialized technology supplements.

The purpose of this document is to describe how DO-330/ED-215 impacts the current tool qualification approach of DO-178B/ED-12B and how it provides more relevant guidance for both tool users and tool providers.

We first review the rationale for a Tool Qualification document. But before the application of DO-330/ED-215, a fundamental pre-condition is to establish for the project the tool qualification criteria and the Tool Qualification Levels (TQLs). As an example, we show how DO-178C/ED-12C determines the criteria and TQLs for the airborne domain. In this domain, the criteria are based on the possible impact of a tool error on the software life cycle processes.

We then highlight the main impact of DO-330/ED-215 on current practice, and provide the relevant information to help the reader to apply this new guidance.

Some supporting information is provided in an appendix of DO-330/ED-215. We describe one of the most important topics, addressing the possible certification credit when using a qualified AutoCode Generator (ACG).

The author, Frédéric Pothon ACG Solutions, and several of the contributors and reviewers participated in the DO-178C/ED-12C working group and subcommittees.

Download document.

© Frédéric Pothon, 2012
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License.

Posted in Open-DO News | Leave a comment

Formalization and Comparison of MCDC and Object Branch Coverage Criteria

By Jamie Ayre | March 19, 2012

This paper was presented by Jerome Guitton at the recent ERTS 2012 conference:
This paper presents formal results derived from the COUVERTURE project, whose goal was to develop tools to support structural coverage analysis of unin- strumented safety-critical software. After briefly introducing the project context and explaining the need for formal foundations, we focus on the relationships between machine branch coverage and the DO-178B Modified Condition/Decision Coverage (MCDC) criterion. A thorough understanding of those relationships is important, since it provides the foundation for knowing where efficient execution trace techniques can be used to demonstrate compliance with the MCDC criterion. We first present several conjectures that were tested using Alloy models, then provide a formally verified characterization of the situations when coverage of object control-flow edges implies MCDC compliance.The full paper can de downloaded here.

Couverture erts2012
View more presentations from AdaCore

Also posted in Certification, Open Source, Papers and Slides | Leave a comment

Integrating Formal Program Verification with Testing

By Jamie Ayre | March 19, 2012

This is the paper that Yannick Moy presented at the recent ERTS 2012 conference:
Verification activities mandated for critical software are essential to achieve the required level of confidence expected in life-critical or business-critical software. They are becoming increasingly costly as, over time, they require the development and maintenance of a large body of functional and robustness tests on larger and more complex applications. Formal program verification offers a way to reduce these costs while providing stronger guarantees than testing. Addressing verification activities with formal verification is supported by upcoming standards such as do-178c for software development in avionics. In the Hi-Lite project, we pursue the integration of formal verification with testing for projects developed in C or Ada. In this paper, we discuss the conditions under which this integration is at least as strong as testing alone. We describe associated costs and benefits, using a simple banking database application as a case study. The full paper can de downloaded here.

Hi-Lite erts2012
View more PowerPoint from AdaCore

Also posted in Certification, Events, Open Source, Papers and Slides | Tagged , , , , | Leave a comment

Open-DO session at ERTS 2012

By Jamie Ayre | January 31, 2012

Many thanks to the organisers of the ERTS 2012 (Embedded Real-Time Software and Systems) conference for including a session linked to the Open-DO initiative. There will be 4 talks on the morning of Thursday February 2:

  • Integrating Formal Program Verification with Testing (Cyrille Comar, Johannes Kanig and Yannick Moy)
  • Compilation of Heterogeneous Models: Motivations and Challenges (Matteo Bordin, Tonu Naks, Andres Toom and Marc Pantel)
  • Formalization and Comparison of MCDC and Object Branch Coverage Criteria (Cyrille Comar, Jerome Guitton, Olivier Hainque, Thomas Quinot)
  • Agility & Lean for Avionic Software Development (Emmanuel Chenu)

    • For more information on the event and to register, please visit http://www.erts2012.org/

    Posted in Open-DO News | Leave a comment

    Prove Your Plane Now!

    By Yannick Moy | January 13, 2012

    The DO-333 is now available! (ok, that’s not free: 215$ for an electronic version, or 300$ for a hard copy, pfew!)

    Under this amazingly explicit name is hiding the formal methods supplement for DO-178C. Or, said otherwise, the document that allows you, as a developer of avionics software, to replace tests/reviews/analyses by formal methods. Or you, as a provider of techniques and tools for formal methods, to find customers in the avionics market. Ah yes, because the new version of the certification standard for avionics software, DO-178C, has been also issued at the same time. So that starts today!

    Here is what the abstract of this doc says:

    This supplement identifies the additions, modifications and substitutions to DO-178C and DO-278A objectives when formal methods are used as part of a software life cycle, and the additional guidance required. It discusses those aspects of airworthiness certification that pertain to the production of software, using formal methods for systems approved using DO-178C.

    Formal methods are mathematically-based techniques for the specification, development and verification of software aspects of digital systems. The mathematical basis of formal methods consists of formal logic, discrete mathematics and computer-readable languages. The use of formal methods is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analyses can contribute to establishing the correctness and robustness of a design.

    Also posted in Certification, Papers and Slides | Tagged | Leave a comment

    Executable Annotations for C Programs

    By Yannick Moy | January 9, 2012

    The Frama-C platform, which integrates static analysis and formal proof of C programs, now has a plug-in for run-time execution of annotations. In particular, preconditions and postconditions written using the E-ACSL subset of the ACSL annotation language for C can now be executed thanks to this plug-in. This is a great move in the direction of better integration of proofs and tests for C programs!

    As far as I know, this is the first attempt at defining a common annotation language for tests and static analysis / proof for C. The annotation languages for C that I know of cannot be executed: Microsoft’s widely used Standard Annotation Language, the annotation language used by the Escher C Verifier or the one from Microsoft’s VCC.

    Note that an important difference between this annotation language and others is that it uses mathematical semantics for operations in annotations. So an addition in annotations cannot overflow. In practice, they are using the GMP library for mathematical integers. Try it for yourself by downloading/installing Frama-C and this plug-in!

    Also posted in Related Initiatives | Tagged , | Leave a comment

    code.NASA

    By Jamie Ayre | January 5, 2012

    An interesting new website added to the family of NASA websites. code.NASA, according the website, NASA “…will continue, unify, and expand NASA’s open source activities. The site will serve to surface existing projects, provide a forum for discussing projects and processes, and guide internal and external groups in open development, release, and contribution.”

    More information can be found at:

    http://open.nasa.gov/blog/2012/01/04/the-plan-for-code/

    I particularly like the call for participation – “Will your code someday escape our solar system or land on an alien planet? We’re working to make it happen, and with your help, it will.”

    Also posted in In the Press, Open Source, Related Initiatives | Leave a comment

    Open World Forum

    By Jamie Ayre | September 15, 2011
    If you are in or around Paris next week you may like to attend the industrial day of the Open World Forum. Taking place on Sep 22 in Paris, there are a number of talks looking at the use of Open Source in industrial contexts and several projects (including Open-DO) will be presented.
    Posted in Open-DO News | Leave a comment

    Boogie Workshop

    By Johannes Kanig | August 8, 2011

    I recently attended the Boogie workshop on intermediate verification languages in Wroclaw, Poland.

    First let me recall that one goal of the Hi-Lite project is to bring formal verification to the Ada language. An intermediate verification language (IVL) can help here because it deals with the most common features that exist in most programming languages: integers, arrays, sequential programming, loops, function calls. There was no need for us in Hi-Lite to reinvent the wheel, we simply picked a suitable IVL.

    There are two main IVLs in the research community, namely Boogie[1] (hence the name of the workshop) and Why[2]. In the Hi-Lite project, the natural choice was Why, as the Why developers are also part of the project.

    Besides talks discussing various improvements in these two main tools, there was also a talk about a new IVL called jStar, mainly targeted at complex programs with shared mutable state, and the very interesting invited talk by Viktor Kuncak[5] showed some ways of using IVLs to develop new programming techniques.

    The workshop website[3] contains a list of all the talks. It is also worth mentioning that it is part of the CADE 23 conference[4] which takes part in Wroclaw all week.

    [1] http://boogie.codeplex.com/
    [2] http://why.lri.fr
    [3] http://research.microsoft.com/en-us/um/people/moskal/boogie2011/
    [4] http://cade23.ii.uni.wroc.pl/
    [5] http://lara.epfl.ch/~kuncak/

    Posted in Open-DO News | Leave a comment

    Riposte project joins Open-DO

    By Jamie Ayre | August 1, 2011

    Riposte is a tool to support developers in verifying SPARK programs. The SPARK Examiner generates verification conditions (VCs) that show that the SPARK program is type safe, free from run-time exceptions and meets the specification given in post conditions and checks. Existing tools allow true VCs to be proven automatically. Riposte augments these capabilities by generating counter examples for false VCs. These counter examples give variable assignments that cause violations in type safety, trigger exceptions or inputs that do not meet the required post conditions. The programmer can then use these to locate and fix bugs or refine the program’s specification.

    The current release of Riposte is at an alpha stage and is intended to be a technology demonstration. Suggestions and feature requests are most welcome. To download the tool, please visit the Riposte project page on the Open-DO Forge.

    Posted in Open-DO News | Leave a comment

    • Categories

    • Open-DO Projects

      Agile
      Couverture
      GeneAuto/Ada
      HiberSource
      Hi-Lite
      Project P
      The Qualifying Machine
      Sparkel
      XReq

    • Contact

      info @ open-do.org