A number of very interesting articles in February’s SoftwareTech News look at the use of FLOSS by the DoD. Topics below give an insight the DoD’s position and strategy in employing open source software.
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
A presentation by Yannick Moy, Senior Engineer, AdaCore, at a recent talk at IRILL Days 2010. Video courtesy of IRILL (http://www.irill.org)
17:30 CET January 27th, 2011 – AdaCore Paris offices, 46 rue d’Amsterdam, 75009 Paris.
Project Couverture has officially come to an end. It’s objectives were to produce a Free Software coverage analysis toolset together with artifacts that allow the tools to be used by developers of safety-critical and mission-critical projects, including systems that need to be certified under safety standards such as DO-178B. The 2 year project was partially funded by the regional authorities of Paris and the Ile-de-France district and the French Ministry of Industry.
The event will highlight the results of the project and showcase the products that have subsequently been developed. If you are interested in attending, please send email to events @ adacore.com.
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!
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.