Categories
Open-DO Projects
Contact
info @ open-do.org
Category Archives: Open-DO News
Couverture product rewarded with an Electron d’Or!
The open source coverage analysis tool GNATcoverage issued from the Couverture Project was awarded with an Electrons d’Or from the Electroniques magazine. GNATcoverage won the prize for the Software Tool category in a prize-giving ceremony in Paris.
Posted in Open-DO News 1 Comment
Safety and security concerns in medical device software
In a recent article in Electronic Design, Ben Brosgol discusses with Bill Wong about safety and security concerns in medical device software and how “recent Food and Drug Administration (FDA) regulations are dealing with such issues, and how programming language and support tool technology can help”
The full article can be found at:
http://electronicdesign.com/article/embedded/Safety-in-Medical-Device-Software-Questions-and-Answers.aspx
Posted in Open-DO News 2 Comments
White Paper: High-Integrity OO Programming in Ada
We have posted a new paper to the Open-DO website “High-Integrity Object-Oriented Programming in Ada“. This paper’s goal is to provide guidance on how to use Ada’s Object Oriented (OO) features for High-Integrity applications; i.e. high-reliability systems with requirements for safety and/or security which may need to demonstrate compliance with domain-specific certification standards. The paper’s authors have extensive experience in this area through their participation in industrial working groups such asthe joint EUROCAE WG71 / RTCA SC 205 working group defining the upcoming RTCA DO178-C/EUROCAE ED12-C avionics safety standard, and ISO’s Ada Rapporteur Group that manages the Ada language standardization process. More information can be found at http://www.open-do.org/high-integrity-oo-programming-in-ada/
We expect this document to evolve over time, so we kindly ask readers to provide as much feedback as possible to AdaCore at info@open-do.org with the name of the document mentioned on the subject line.
Posted in Open-DO News 1 Comment
DoD and Open Source Software
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.
Posted in Open-DO News Leave a comment
Being Elmer Fudd
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
Hi-Lite: a Verification Toolkit for Unit Test & Unit Proof
A presentation by Yannick Moy, Senior Engineer, AdaCore, at a recent talk at IRILL Days 2010. Video courtesy of IRILL (http://www.irill.org)
Also posted in Videos Leave a comment
Formal Containers
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.
Posted in Open-DO News Leave a comment
Designing and Implementing a Verifiable High Assurance Workstation (Alex Senier – secunet)
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.
Also posted in Events, Videos Leave a comment
Couverture end of project event
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.
Posted in Open-DO News Leave a comment
Case Study: Can you afford to ignore formal analysis?
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!
Also posted in Certification, Papers and Slides Tagged Formal verification, Hi-Lite, Testing Leave a comment