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

Posted in Certification, Open Source, Open-DO News, 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

Posted in Certification, Events, Open Source, Open-DO News, Papers and Slides | Tagged , , , , | Leave a comment

Compilation of Heterogeneous Models: Motivations and Challenges

By Jamie Ayre | March 19, 2012

This is the paper that Matteo Bordin presented at the recent ERTS 2012 conference:
The widespread use of model driven engineering in the development of software-intensive systems, including high- integrity embedded systems, gave rise to a “Tower of Babel” of modeling languages. System architects may use languages such as OMG SysML and MARTE, SAE AADL or EAST-ADL; control and command engineers tend to use graphical tools such as MathWorks Simulink/Stateflow or Esterel Technologies SCADE, or textual languages such as MathWorks Embedded Matlab; software engineers usually rely on OMG UML; and, of course, many in- house domain specific languages are equally used at any step of the development process. This heterogeneity of modeling formalisms raises several questions on the verification and code generation for systems described using heterogeneous models: How can we ensure consistency across multiple modeling views? How can we generate code, which is optimized with respect to multiple modeling views? How can we ensure model-level verification is consistent with the run-time behavior of the generated executable application?

Project P erts2012
View more presentations from AdaCore

Read More »
Posted in Events, Papers and Slides | Leave a comment

Trusting the tools: An agile approach to tool qualification for DO-178C

By Jamie Ayre | March 12, 2012

Ben Brosgol and Greg Gicca look at agility, tool qualification and the new DO-178C standard in this article in Military Embedded Systems.

Abstract:
The DO-178C standard improves upon the previous DO-178B version by better supporting newer concepts in software development processes and methods. The new standard contains a core document and four supplements. The core document is an updated version of DO-178B with clarifications, improvements and many known issues addressed. The supplements clarify certification using object oriented technology and related techniques, model based development and verification, formal methods, and software tool qualification considerations. This paper will discuss the new DO-178C guidance for tool qualification and will present an approach to tool qualification based on iterative and agile development methods. Through this approach tools may be qualified at a lower cost and more importantly re-qualified for new software development environments as tools sets (such as compilers) are updated during the main application’s certified development life span.

Full article here.

Posted in Agile/Lean Programming, Certification | Leave a comment

Nose Gear Challenge Problem joins Open-DO

By Jamie Ayre | February 12, 2012

The Nose Gear Challenge Problem has joined the Open-DO forge. It was initially developed to stimulate and unify discussions at the 2nd Workshop on Theorem Proving in Certification held on December 5 – 6, 2011 in Cambridge, UK. The goal of this project is to consider how/if theorem proving can have any value in providing assurance in the context of DO-178C formal method supplement. The contributors to the project can use the Nose Gear problem example to explain their techniques.

Visit the Nose Gear Challenge Problem project page on the Open-DO forge.

Posted in Certification, Open Source, Related Initiatives | 1 Comment

Certification, Safety and Security at ERTS 2012

By Yannick Moy | February 3, 2012

We are now leaving the Embedded Real Time Systems and Software conference which was held in Toulouse for the last 3 days. The conference has been expanding since the last occurrence in 2010, with more international presence, many German companies in particular, and a large number of companies from the automotive industry (maybe this is related? :) ).

I was particularly interested in the increasing concern over techniques to address safety and security. Safety is not new in avionics/aerospace, but security is, and both safety and security are quite new for automotive. The key to understanding these concerns is the recent release of new safety certification in both avionics (DO-178C) and automotive (ISO-26262). Both put some emphasis (not at the same level, as one could expect) on static analysis and formal techniques.

Like two years ago, there were many presentations of work on formal methods and modelling, with many formal methods applying to modelling. Next episode in two years!

Posted in Events | 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.

    Posted in Certification, Open-DO News, 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!

    Posted in Open-DO News, 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.”

    Posted in In the Press, Open Source, Open-DO News, Related Initiatives | 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