Many thanks to the organisers of the ERTS 2012 (Embedded Real-Time Software and Systems) conference for including a session linked to the Open-DO initiative. There will be 4 talks on the morning of Thursday February 2:
The DO-333 is now available! (ok, that’s not free: 215$ for an electronic version, or 300$ for a hard copy, pfew!)
Under this amazingly explicit name is hiding the formal methods supplement for DO-178C. Or, said otherwise, the document that allows you, as a developer of avionics software, to replace tests/reviews/analyses by formal methods. Or you, as a provider of techniques and tools for formal methods, to find customers in the avionics market. Ah yes, because the new version of the certification standard for avionics software, DO-178C, has been also issued at the same time. So that starts today!
Here is what the abstract of this doc says:
This supplement identifies the additions, modifications and substitutions to DO-178C and DO-278A objectives when formal methods are used as part of a software life cycle, and the additional guidance required. It discusses those aspects of airworthiness certification that pertain to the production of software, using formal methods for systems approved using DO-178C.
Formal methods are mathematically-based techniques for the specification, development and verification of software aspects of digital systems. The mathematical basis of formal methods consists of formal logic, discrete mathematics and computer-readable languages. The use of formal methods is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analyses can contribute to establishing the correctness and robustness of a design.
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/
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.
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
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.