In a paper first published in 2008, Christophe Bertrand and Christopher P. Fuhrman from the Department of Software and IT Engineering, ÉTS, Montreal, Canada, discuss how OpenUP (”a minimally sufficient software development process – meaning that only fundamental content is included”), could be adopted for use in the context of building high-integrity (DO-178B) software.
Abstract:
“Civil avionics software must be certified according to standards mandated by governmental agencies, such as the Federal Aviations Administration in the United States. Typically the certification is done in the context of the DO-178B standard. For companies seeking a first-time certification, preparation for DO-178B can be a daunting challenge. The documentation and planning of high-integrity software is therefore a software engineering problem. As a solution, we consider an open-source derivative of the Unified Process, called OpenUP, as a base process model from which to begin. Because of their importance in the DO-178B standard, software requirement activities are the focus of our study. We show that most of DO-178B’s objectives in this dimension could be supported with activities in OpenUP.”
Full paper:
Towards Defining Software Development Processes in DO-178B with OpenUP
Below are a couple of links to a paper and an article discussing the formal verification of safety-critical applications.
The first one is an article written by Boris Sedacca in the IET magazine “Verifying safety-critical aerospace and automotive applications” looking at how the current and upcoming Avionics and Automotive standards “aim to improve code verification”.
http://kn.theiet.org/magazine/issues/1013/verifying-safety-1013.cfm
The second one is a paper written by Xavier Leroy who is a member of the team at INRIA working on the CompCert project. “The paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness.”
http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf
In this
recent article published in
Defense Tech Briefs, Robert Dewar discusses how integrating formal methods into the software design process can bring better assurance than traditional testing methods. Through the
Hi-Lite project, he looks at how testing, static analysis, and formal methods combined could “advance the state of the practice in developing modern avionics systems and other critical software.”
Also posted in In the Press |
According to the website, “The Certification Together International Conference for the Aeronautical Industry is the only event in Europe fully dedicated to System, Software and Hardware certification challenges.”
Looking at the program, a large part of it, as you’d expect, is dedicated to the changes in the upcoming DO-178C standard and how it will affect current certification process and practices. Coupled with these are more practical, hand-on user studies provided by primes and vendors alike.
Cyrille Comar will be giving a talk based around “The challenges of Agile certification” and an update on the Object Oriented Technology (OOT) supplement of DO-178C.
The event will be held in Toulouse, France – Oct 26-28.
In this recently published article in Embedded Technology, Jose Ruiz looks at how Agile methods can be successfully applied when building safety-critical embedded software. He concludes:
“Production of safety-critical systems is typically expensive and not conducive to changes. Agile techniques can help increase the level of automation in production and certification, increasing adaptability to changing requirements and reducing delivery time and cost. These methods are based on iterative and incremental development, verified by continuous and automated tests. This notion can be extended to all certification artifacts to achieve continuous certification.”
To read the full article, please click here.
At the recent ERTS² 2010 conference held in Toulouse, Thomas Quinot presented a paper entitled
“Object and Source Coverage for Critical Appl ications with the Couverture Open Analysis Framework“.
It presents the Couverture approach to object and structural coverage analysis for certified safety-critical applications, in particular in the context of DO-178.
XReq – Executable Requirements for DO-178B – is the latest project to join the Open-DO initiative. XReq, first contributed by Sogilis, is a tool designed to help testing and verifying a project. It has been specifically adapted for the DO-178B context but can be used by a much wider audience. To help DO-178B projects, it bring together the tests (HLT/LLT) with their requirements, thus helping traceability of the tests.
For further information, please visit the XReq project page.
Also posted in Open-DO News |
I spent a very interesting week in Toulouse last week. It started with a day of conference in which INRIA research labs showed a host of products and advanced research applicable to the domains of modeling and safety. There was in particular demos of Astrée (static analyzer for C, now sold by AbsInt Gmbh), Frama-C (framework for analyses on C, partner in Hi-Lite) and Alt-Ergo (prover SMT, partner in Hi-Lite).
It continued with the conference ERTS² during 3 days, which gathered many French and European providers and customers of embedded solutions. I’d like to highlight 3 presentations:
Also posted in Events, Open-DO News |
Yesterday saw the official launch of the Hi-Lite project. Financially supported by French national and local government agencies, Hi-Lite aims to increase the use of formal methods in developing high integrity software, particularly to meet the forthcoming DO-178C avionics standard.
Hi-Lite is completely based on libre software. The project is structured in two different toolchains for Ada and C based on GNAT/GCC compilers, the SPARK verification toolset and the Frama-C platform. The integration of these toolchains inside two industrial IDEs offers to the user a common interaction on Ada and C programs. In particular, mixed Ada/C programs can be verified against a common specification.
The project partners are AdaCore, Altran Praxis, Astrium Space Transportation, CEA-LIST, the ProVal team of INRIA and Thales Communications. AdaCore is the project leader. For more information please visit www.open-do.org/projects/hi-lite and to subscribe to the public mailing list please send email to hi-lite-discuss@lists.forge.open-do.org.
We will be reporting on its progress here as it reaches major milestones throughout the evolution of the project.