We learned this week of ImProve, a lightweight DSL intended for building high assurance embedded applications. Developed by Tom Hawkins, the tool is an EDSL that performs formal verification (via. model checking) and code generation. The host language is Haskell; meaning ImProve programs are nothing more than Haskell programs that call the ImProve library API.
ImProve’s semantics are extremely simple:
- It is an imperative language like C or Ada.
- It only has 3 datatypes (bool, int, float).
- There are a total of 16 expression types (add, subtract, AND, OR, etc.).
- Statements consist of variables assignments, conditional “IF” statements, and assertions.
In terms of the ImProve compiler structure, a thin layer of Haskell helps translate ImProve programs down to an intermediate representation, from which programs are verified and C code is generated.
For verification, the IR language is passed to a k-induction model checker (part of the ImProve library), which makes calls down to an SMT solver (currently Yices). ImProve provides assertions statements to capture design intent. Assertions can be seeded with previously proven lemmas to aid verification convergence.
For more information, please visit the project website:
https://github.com/tomahawkins/improve/wiki/ImProve
Ever found yourself in an extreme stressed state because of some bugs* escaping you? Then you know how it feels to be Elmer Fudd. Not a typical hero, never victorious in his hunt. So it feels being a software engineer. A new episode in this tragicomedy is a paper by Yang et al. from Uni Utah that will be presented at PLDI conference this year.
In this paper, the authors report on 3 years looking for bugs in C compilers. They generated random compliant ANSI C programs, which all C compilers should compile to a program computing the same values, and compared the results of various C compilers on the generated programs. They found 325 bugs, 8 of which they present in a few lines in the paper. Really savory to see how logic defeats man. In case you chill like me over these bug stories, you can read some I wrote at Microsoft and at AdaCore.
The light in the dark comes from a little known C compiler, CompCert whose middle-end successfully defeated the repeated attacks (6 CPU-years!) of the researchers. Guess what? It is written in Coq, a formal language, which allowed proving its correctness. Also interesting is the fact that even CompCert had bugs in its non formally verified parts, like the parser, where it makes sense to have testing in place.
* bunny of course
Below are the slides from the recent
Couverture project conclusion meeting. Cyrille Comar presented the original needs and goals of the project, the challenges the team came across a long the way, and the main results.
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!