The first conference based around the TOPCASED toolkit project will take place in Toulouse February 2nd-4th, 2011.
TOPCASED (Toolkit in OPen-source for Critical Application and SystEms Development) is a modular, open-source, Eclipse-based software environment providing methods and tools for critical embedded systems development, ranging from system and architecture specifications to software and hardware implementation through equipment definition. TOPCASED promotes model-driven engineering and formal methods as key technologies.
Last time I met John Chilenski at the SC-205 (DO-178C) working group, I mentioned to him the concrete and theoretical results of the couverture project. Since our work had been partly inspired by the research studies he worked on for the FAA (http://www.faa.gov/aircraft/air_cert/design_approvals/air_software/research), I was convinced that our results would be of interest to him. I suggested that he take a look at the paper we published at ERTS 2010 (http://www2.adacore.com/wp-content/uploads/2010/06/couverture_ertss2010.pdf) and he came back with an interesting question:
‘Hi Cyrille,
I hope you had a Merry Christmas and a Happy New Year!
I have a question for you. In the paper you state: “When some conditions involve multiple conditional branch instructions, OBC still implies MC/DC, but becomes in effect an even stronger property: MC/DC could potentially be established by a test set that does not achieve OBC.”
When does a condition involve multiple conditional branch instructions? I would appreciate an example to help me understand this.
Thanks,
-John’
to which I answered:
‘the code generator may have to generate multiple conditions for various constructs of a language depending on what this construct does. For instance, in Ada :
if Table (I) > 3 then
there is clearly a single condition here but if checks are enabled, the object code for this condition will contain additional branches because of the index check. Basically anything that is supposed to be detected by a good Source-to-Object traceability analysis as “non immediately traceable” is a likely candidate. another example that doesn’t involve Ada dynamic checks:
if (A mod B) = 0 then ….
if you look at the code generated by such a sequence, you might be surprised by the number of conditionals that might be generated for such a trivial expression 
’
I attended yesterday the PhD defense of Stéphane Lescuyer, who presented his work on the proof of prover Alt-Ergo, pushing the boundary of what’s feasible with today’s proof technology.
First, a few words of why this is interesting for us at AdaCore, in an industrial setting. Starting with SPARK Pro 9.1, users now have the possibility to call the prover Alt-Ergo to prove some formulas generated by the SPARK tool-set, in addition to the existing SPARK prover. Proving these formulas ensures that there are no run-time errors and that subprograms properly implement their contracts. Thus, it is crucial that the prover used is correct: whenever it says a formula is true, it must be the case. In project Hi-Lite (hosted on Open-DO), we also aim at using Alt-Ergo to prove functional properties of interest to a user on parts of an Ada codebase.
Second, the inner algorithms of such automatic provers are very tricky, so it is quite hard to show a convincing proof that they are correct. The well-known case is the Shostak’s method on which Alt-Ergo’s main algorithm is based: Shostak published his algorithm in 84, and despite many papers discussing the approach, the algorithm was erroneous on various accounts; it was corrected in two steps, in 1996 by Cyrluk, Lincoln and Shankar and in 2001 by Rueß and Shankar. Only a formal proof like the one done by Stéphane Lescuyer can then provide a strong argument for correctness.
Bottom line is that Alt-Ergo is built around a proven core, and that’s great news in order to use it in safety-critical software development and verification.
Also posted in Events | Tagged Hi-Lite, proof |
This is a title I’d like to reuse some day for a case study in Hi-Lite, but right now it is the title of a very interesting paper published by EE Times: people from Alcatel-Lucent formally verified many properties of an ASIC design in a large communication system.
What is stricking is the similarity of the findings and the challenges with what we do in Hi-Lite, despite the very different nature of the properties verified in hardware and in software, and the different techniques involved. Pages 3 and 4, they detail the additional errors found by formal verification on a codebase already simulated, with actual examples of what simulation missed and why. Very instructive. Which leads them to propose to bring together simulation and formal verification on page 5.
Interestingly, the difficulties to bring these two worlds together are the same as the ones in software: different semantics in simulation and formal verification (ex 1 p 5) and non-executable annotations (ex 2 p 5). Good thing that we insisted on the same semantics in Hi-Lite for execution and formal verification, as well as executable annotations!
Below are a couple of presentations from the recent Certification Together conference. Both concern the OOT supplement of the upcoming DO-178C avionics standard.
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.
Also posted in In the Press |
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!
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.”