Earlier this month, on March 3rd, AdaCore was awarded a grant by the French government and local
authorities to develop an innovative set of tools integrated with its GNAT Pro
platform. AdaCore is leading a consortium of 2 research institutes (CEA-List,
the ProVal team of INRIA) and 4 industrial companies (AdaCore, Altran, Astrium
and Thales Communications) in this effort. The project, named Hi-Lite, is
starting in mid-2010 and will continue for 3 years.
Hi-Lite’s goal is to promote the use of formal methods in developing
high-integrity software. It loosely integrates formal proofs with testing and
static analysis, thus allowing developers to combine different techniques around
a common expression of properties and constraints.
Hi-Lite is completely based on free software. The project is structured as two
different toolchains for Ada and C based on GNAT/GCC compilers (Ada and C), the
CodePeer static analyzer (Ada), the SPARK verification toolset (Ada) and the
Frama-C platform (C).
A big thank you to all those who attended the very successful Open-DO event in Paris on March 11, 2010. And if you missed it, don’t worry. We’ll be posting videos of all the talks over the coming weeks.
The conference was dedicated to exploring the possibilities of combining formality with agility for critical software development. We start with Paul Boca from Hornbill Systems Ltd, who makes the case that formal methods can complement agile practices and vice versa.
Each week we will post a new talk from this event. Enjoy!
You can also view the presentation slides if you want to follow along.
We are pleased to welcome the HiberSource project to Open-DO. This configuration management system is used to manage project data in accordance with DO-178B and supports the full software life cycle.
There are many free version control systems (such as SVN) but there are no free configuration systems to support projects (like Razor or PVCS). HiberSource was started to be a configuration system to support full software life cycle with developing, verification and other certification activities.
For more information, please visit the project on the Open-DO forge.
Last month I attended part of the Formal Methods Week 2009 in Eindhoven. Each year the FMWeek brings the world of formal verification together, with an emphasis on academic and industrial partnerships.
Although I am familiar with the field, I was still impressed by what is currently possible with tools based on formal methods. Although it will never
be 100% automated, you can already get very strong guarantees on industrial products with high levels of automation.
Two examples show it better:
Airbus presented their use of formal verification tools for DO-178B software. Five of the six tools that were presented are in use within operational units. This presentation echoed, 10 years later, the presentation they gave at FM 1999 about their first trial with formal verification. With a decade of experience in industrial use of such tools, they have defined 5 “must-have” criteria: soundness, applicability to the code, usability by “normal” engineers on “normal” computers, improve on classical methods, certifiability. Very important lessons indeed.
Speaking at the Ada UK Conference 2009 in London, Jim Sutton presents a talk on a Lean approach to one of the most import aspects of starting any development project: selecting the right programing language.
Speaking at the Ada UK Conference 2009 in London, Franco Gasperoni presents and positions requirement-based testing and coverage analysis in terms of the Avionics standard DO-178B. He then goes on to show how the Open-DO initiative (through Project Coverage) is addressing these needs.
Last week I attented the Grenoble (October 20, 2009) and Valence (October 22, 2009) conferences as part of the Agile Tour 2009 series. These events were a big success and attracted more than 450 attendees! I would like to thank one more time the CARA who did a very good job at organizing these.
The presentations were of very high quality and their diversity pleased practionners as well as managers and students. All the slides are accessible on the CARA’s website (French and English).
I gave a talk in Grenoble and Valence about the infrastructure and processes we put in place at AdaCore to build and test on a daily basis all our compilation chains and accompanying technology in a Lean fashion.
I also presented the “qualification machine” we have built based on open source technology to ease the DO-178B tool qualification process by adopting an agile philosophy.
In a recent announcement, IEEE has approved work to develop a standard for a language to capture software requirements.
Unfortunately, I have not found much information about it. They mention that the information will be presented in a tree-like structure, which should fit well with the hierarchical organization of requirements in typical safety-critical development.
In a recent article in Avionics Intelligence, Cyrille Comar and others describe the upcoming DO-178C standard and the differences between it and the existing DO-178B one:
“Avionics software designers are quite familiar with the DO-178B certification process for flight software from the Federal Aviation Administration (FAA) and the European Aviation Safety Agency (EASA). However, current technology trends in software code development are requiring new verification and certification approaches, so industry and government experts are building a new certification called DO-178C to address these concerns.” To read the full article, please click here.
Cyrille Comar gave a talk at the recent SAFECOMP conference on the work being undertaken by the SC-205 and WG-71 working group on the upcoming DO-178C standard. He gives particular attention to the Tools Qualification Supplement, the OOT (Object-Oriented Technology) Supplement, and the Formal Methods Supplement.
