Challenges of Agile Qualification
View more presentations from AdaCore.
Categories
Open-DO Projects
Want to get involved?
Contact
Hi-Lite Progress: Discussions on Specification Languages
We had yesterday our first joint meeting in Hi-Lite since the start of the project, 6 months ago. This was the occasion for CEA to present their ideas for E-ACSL (the executable fragment of the ACSL specification language for C) and for us at AdaCore to present our ideas for ALFA (the subset of Ada 2012 that will be suitable for formal verification).
The overall directions have been agreed by all partners. In particular, we agreed on the vision of a product that allows unit testing and/or unit proof on individual functions from a program, depending on the features of C/Ada exercized in the function. This will be a major departure from other formal verification tools and methodologies (SPARK, B method) allowing a finer-grain choice of what should be formally verified and what should be tested.
Discussions on E-ACSL and ALFA are expected to continue on the public mailing list hi-lite-discuss@lists.forge.open-do.org.
Posted in Open-DO News Leave a comment
DO-178C Expected for Q1 2011
According to this article, which gives an overview of the changes introduced by this new version of the avionics standard.
I like her presentation of Formal Methods:
Formal methods are a class of mathematically based techniques used for the specification, development, and verification of avionics software. Formal methods tools, for example, are used to represent an aircraft’s mathematically expressed control laws and their translation into software code for the aircraft’s computers. Formal methods can be used to “prove that software is an accurate representation of the mathematical expressions,” Hillary says.
Because formal methods enable software engineers to verify the value of software components, experts say they hope the integrated testing phase will be less manually intensive, Hilderman says.
Formal methods enable software engineers to look at the parts as well as the whole of the code, and help get the software verification process started earlier. Formal methods help verify software components as they are developed, which reduces the need for reverification during integration and testing, which typically cannot start until the software is nearly complete. Under DO-178C, developers will be able to use testing results from earlier in the process as formal results.
Formal methods tools are most helpful with large and complex software programs — 50,000 or more lines of code containing advanced algorithms, Hilderman says. Not many people use them now and it will be some time before they become mainstream.
Posted in Certification, In the Press 2 Comments
Use of Formal Methods in Avionics Triggers Interest in Railway
I was invited today to give a talk at Fraunhofer FIRST, a German research institute, on Formal Verification in Aeronautics: Current Practice and Upcoming Standard. I told them about the pioneering work done at Airbus, especially related to unit proof to replace unit testing, and about the new version of the DO-178 standard (the ‘C’ version) expected in 2011, which states that formal methods can be used instead of testing.
Contrast what the DO-178B says:
Formal methods are complementary to testing.
to what the (draft of the) DO-178C says:
Formal methods [...] might be the primary source of evidence for the satisfaction of many of the objectives concerned with development and verification
The audience was around 15 people, half of which from the railway industry in Germany, Belgium and Italy. Their reason for coming to this two-day tutorial around the tool Frama-C, developed by CEA LIST and used at Airbus, is that they have watched with increasing interest the advances of formal methods in the avionics industry, and they would like to apply some of it to the railway domain when possible. Very encouraging, and thanks Jens Gerlach from Fraunhofer FIRST for organizing this kind of events!
Posted in Certification, Events 2 Comments
OpenUP and DO-178B development processes
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
Challenges facing avionics software developers
In a recent article “Avionics software programmers challenged by integration, certification, testing issues for software-centric aircraft“, Barry Rosenberg from Avionics Magazine discusses the testing and certification processes used when building these systems.
Posted in Certification, In the Press Leave a comment
Must-see Videos on Code Verification
Rustan Leino, a researcher at Microsoft Research, has started creating a set of videos where he both teaches and demoes how to do code verification with the tools developed at Microsoft Research. This shows how to overcome the difficulties than someone may encounter with every code verification tool, except the GUI is amazingly intuitive (verification in the background while typing, very precise error messages).
No only that, but Rustan also sings and dances… really enjoyable!