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.
From a talk given at the SPARK User Group 2010 High Assurance Software Symposium, Rod Chapman from Altan Praxis talks about the guiding principles behind PSP (Personal Software Process) and TSP (Team Software Process).
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.
At the upcoming Embedded World conference in Nuremberg, Germany, there will be a days conference on the use of freely-licensed open source software (FLOSS) to build safety-critical systems. Presentation topics include:
Validation of Linux for Safety-Related Systems
Linux as a real-time Hypervisor for the automotive industry
Efficient Safety Critical Systems Development – Is FLOSS the only answer?
Finding Misuses of Unsigned Integers in Linux Device Driver Code
“Open Proof” for Railway Safety Software A Potential Way-Out of Vendor Lock-in Advancing to Standardization, Transparency, and Software Security
Improved Redundancy and Consistency beyond RAID 1
Utilizing security methods of FLOSS GPOS for safety
We have added a new page describing Formal Containers to the Hi-Lite project. It describes a new version of the API for Ada definite containers, designed to simplify the annotation process. An implementation of these containers will be usable in critical programs. It is really interesting to have containers for critical systems, since they are often a good trade-off for ad-hoc, pointer-based structures which make users’ code hard to certify. Since they have been formally axiomatized, these containers will be part of the Ada subset that can be formally proved correct in the context of Hi-Lite.
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.
From a talk given at the SPARK User Group 2010 High Assurance Software Symposium, Alex Deas from Deep Life talks about developing software for deep water rebreathers which must meet the rigorous European safety standard SIL3.
From a talk given at the SPARK User Group 2010 High Assurance Software Symposium, Rod White from MBDA talks about Autocoding and raises the question: Do we still need software design?
From a talk given at the SPARK User Group 2010 High Assurance Software Symposium, Alex Senier from secunet talks about their experiences building High Assurance workstations.