From the Ada Connection 2011 talks, Jean-Charles Dalbin from Airbus talks about Ada based Automatic Code Generation Tools in DO178B context.
Categories
Open-DO Projects
Want to get involved?
Contact
Ada Connection 2011 – Ada Based Automatic Code Generation Tools in the DO178B context »
Posted in Agile/Lean Programming, Videos Leave a comment
EE Times Design article – The Big Thaw
Matteo Bordin, Jerome Lambourg, and Ben Brosgol discuss some of the principles behind the Open-DO initiative in an article entitled The “Big Thaw” – An Agile Process for Software Certification for EE Times Design.
Abtract “To achieve certification, safety-critical systems must demonstrate compliance with domain-specific standards such as DO-178 for commercial avionics. Developing a certified system consists of various interrelated activities that produce outputs (collections of artifacts) as evidence of successful completion. For example, one of the DO-178 verification activities is a traceability analysis; its output is a report showing that each software requirement is implemented in the source code. Conducting the certification-required activities and producing the artifacts demand a major effort, much more than for conventional Quality Assurance on non safety-critical systems.” Read the full article.
Open World Forum
If you are in or around Paris next week you may like to attend the industrial day of the Open World Forum. Taking place on Sep 22 in Paris, there are a number of talks looking at the use of Open Source in industrial contexts and several projects (including Open-DO) will be presented.
Posted in Open-DO News Leave a comment
Boogie Workshop
I recently attended the Boogie workshop on intermediate verification languages in Wroclaw, Poland.
First let me recall that one goal of the Hi-Lite project is to bring formal verification to the Ada language. An intermediate verification language (IVL) can help here because it deals with the most common features that exist in most programming languages: integers, arrays, sequential programming, loops, function calls. There was no need for us in Hi-Lite to reinvent the wheel, we simply picked a suitable IVL.
There are two main IVLs in the research community, namely Boogie[1] (hence the name of the workshop) and Why[2]. In the Hi-Lite project, the natural choice was Why, as the Why developers are also part of the project.
Besides talks discussing various improvements in these two main tools, there was also a talk about a new IVL called jStar, mainly targeted at complex programs with shared mutable state, and the very interesting invited talk by Viktor Kuncak[5] showed some ways of using IVLs to develop new programming techniques.
The workshop website[3] contains a list of all the talks. It is also worth mentioning that it is part of the CADE 23 conference[4] which takes part in Wroclaw all week.
[1] http://boogie.codeplex.com/
[2] http://why.lri.fr
[3] http://research.microsoft.com/en-us/um/people/moskal/boogie2011/
[4] http://cade23.ii.uni.wroc.pl/
[5] http://lara.epfl.ch/~kuncak/
Posted in Open-DO News Leave a comment
Riposte project joins Open-DO
Riposte is a tool to support developers in verifying SPARK programs. The SPARK Examiner generates verification conditions (VCs) that show that the SPARK program is type safe, free from run-time exceptions and meets the specification given in post conditions and checks. Existing tools allow true VCs to be proven automatically. Riposte augments these capabilities by generating counter examples for false VCs. These counter examples give variable assignments that cause violations in type safety, trigger exceptions or inputs that do not meet the required post conditions. The programmer can then use these to locate and fix bugs or refine the program’s specification.
The current release of Riposte is at an alpha stage and is intended to be a technology demonstration. Suggestions and feature requests are most welcome. To download the tool, please visit the Riposte project page on the Open-DO Forge.
Posted in Open-DO News Leave a comment
Best Paper Award for Results of Verification Competition
Last year, the conference VSTTE 2010 organized a competition of software verification systems (language + tools), to improve understanding of each system’s pros and cons. Rod Chapman from Altran Praxis participated with the SPARK language and toolset, and solved the first problem even beyond what the subject asked. We have since provided solutions in SPARK to all five problems, like other teams, which formed the basis for a report that you can find on this page.
This report was deemed important enough by the organizers of the Formal Methods conference 2011 that they have granted it the best paper award.
Furthermore, the page of the competition contains an archive with all solutions in many different languages and systems… you can even DIY!
Posted in Certification, Events, Papers and Slides 1 Comment
Language Vulnerabilities for Dummies
In case you do not know the series of books “for Dummies”, its principle is to explore a subject from the ground up, with rich explanations and examples for non-experts. That’s in my view a valid alternative title for the recently published “Guidance to Avoiding Vulnerabilities in Programming Languages through Language Selection and Use”. Rich (around 70 vulnerabilities explored) + detailed (130 pages!) + accessible (it contains the best discussion I’ve read of unspecified/implementation-defined/undefined behavior).
The ISO/IEC committee has produced here a language-neutral evaluation of the ways in which a language may “come in the way”, and how to avoid traps and pitfalls either upfront (in language design) or in the field (through coding standards and use of static analysis tools). This is a must-read for anyone whose task is to establish coding guidelines, recommend the usage of a static analysis tool, or choose a programming language for some project.
While Ada and SPARK naturally stand as the languages with fewer vulnerabilities, it also shows the many uses of static analysis tools, from coding standard checking (like GNATcheck) to static analysis (like CodePeer) and formal proof (like SPARK toolset). The recommendations also match well the restrictions for the Alfa subset of Ada that we are defining in project Hi-Lite. (See for example the discussion of aliasing in section 6.39 “Passing Parameters and Return Values”.)
Posted in Certification, Papers and Slides 2 Comments
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 1 Comment