Categories
Open-DO Projects
Contact
info @ open-do.org
Category Archives: Events
Autocoding – Do we still need software design? (Rod White – MBDA)
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?
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 Open-DO News, Videos Leave a comment
Proving Alt-Ergo prover in Coq
I attended yesterday the PhD defense of Stéphane Lescuyer, who presented his work on the proof of prover Alt-Ergo, pushing the boundary of what’s feasible with today’s proof technology.
First, a few words of why this is interesting for us at AdaCore, in an industrial setting. Starting with SPARK Pro 9.1, users now have the possibility to call the prover Alt-Ergo to prove some formulas generated by the SPARK tool-set, in addition to the existing SPARK prover. Proving these formulas ensures that there are no run-time errors and that subprograms properly implement their contracts. Thus, it is crucial that the prover used is correct: whenever it says a formula is true, it must be the case. In project Hi-Lite (hosted on Open-DO), we also aim at using Alt-Ergo to prove functional properties of interest to a user on parts of an Ada codebase.
Second, the inner algorithms of such automatic provers are very tricky, so it is quite hard to show a convincing proof that they are correct. The well-known case is the Shostak’s method on which Alt-Ergo’s main algorithm is based: Shostak published his algorithm in 84, and despite many papers discussing the approach, the algorithm was erroneous on various accounts; it was corrected in two steps, in 1996 by Cyrluk, Lincoln and Shankar and in 2001 by Rueß and Shankar. Only a formal proof like the one done by Stéphane Lescuyer can then provide a strong argument for correctness.
Bottom line is that Alt-Ergo is built around a proven core, and that’s great news in order to use it in safety-critical software development and verification.
Use of Formal Methods in Avionics Triggers Interest in Railway
I was invited today to give a talk at Fraunhofer FIRST, a German research institute, on Formal Verification in Aeronautics: Current Practice and Upcoming Standard. I told them about the pioneering work done at Airbus, especially related to unit proof to replace unit testing, and about the new version of the DO-178 standard (the ‘C’ version) expected in 2011, which states that formal methods can be used instead of testing.
Contrast what the DO-178B says:
Formal methods are complementary to testing.
to what the (draft of the) DO-178C says:
Formal methods [...] might be the primary source of evidence for the satisfaction of many of the objectives concerned with development and verification
The audience was around 15 people, half of which from the railway industry in Germany, Belgium and Italy. Their reason for coming to this two-day tutorial around the tool Frama-C, developed by CEA LIST and used at Airbus, is that they have watched with increasing interest the advances of formal methods in the avionics industry, and they would like to apply some of it to the railway domain when possible. Very encouraging, and thanks Jens Gerlach from Fraunhofer FIRST for organizing this kind of events!
Also posted in Certification 2 Comments
ERTS² conference week
I spent a very interesting week in Toulouse last week. It started with a day of conference in which INRIA research labs showed a host of products and advanced research applicable to the domains of modeling and safety. There was in particular demos of Astrée (static analyzer for C, now sold by AbsInt Gmbh), Frama-C (framework for analyses on C, partner in Hi-Lite) and Alt-Ergo (prover SMT, partner in Hi-Lite).
It continued with the conference ERTS² during 3 days, which gathered many French and European providers and customers of embedded solutions. I’d like to highlight 3 presentations:
- the Formal Methods Subgroup of the upcoming DO-178C standard presented how formal methods may be used in a certification context
- PolySpace and automotive stakeholders presented the use of static analysis tools to ensure levels of quality from subcontractors
- the initiative “Certification Together” presented the goals of their initiative to share the cost of certification
Also posted in Certification, Open-DO News 1 Comment
Formal Method for Avionics Software Verification (Hervé Delseny)
The next talk in our series from the recent Open-DO Conference is from Hervé Delseny, an expert in Avionics Software Aspects of Certification at Airbus. In his talk he gives examples of Airbus’ use of Formal Methods to verify avionics software, and summarises the integration of Formal Methods in the upcoming ED-12/DO-178 issue C.
You can also view the presentation slides if you want to follow along.
Formal Method for Avionics Software Verification
View more presentations from AdaCore.
Also posted in Open-DO News, Papers and Slides, Videos Leave a comment
The Use of Formal Methods on the iFACTS ATC Project (Neil White)
The next talk in our series from the recent Open-DO Conference is from Neil White, Principal Engineer with Altran Praxis. His talk provides an overview of the formal methods used on the iFACTS project. iFACTS is delivering increased Air Traffic Control capability to the UK.
You can also view the presentation slides if you want to follow along.
Also posted in Papers and Slides, Videos Leave a comment
Agile Methods and Safety-Critical Software (Peter Gardner)
The next talk in our series from the recent Open-DO Conference is from Dr. Peter Gardner. Peter has twenty years experience in languages and software development methodologies and acts as the focal point for UML in Silver Atena. His talk surveys Agile methods and formulates a list of features that occur in these methods, then considers whether each of the features can be applied in the field of safety-critical software development.
You can also view the presentation slides if you want to follow along.
Also posted in Agile/Lean Programming, Papers and Slides, Videos 12 Comments
Open-DO Update (Cyrille Comar)
The next talk in our series from the recent Open-DO Conference is from Cyrille Comar, Managing Director of AdaCore EU, who gives an update on the latest happenings with the Open-DO initiative and talks about AdaCore’s new French government funded project, Hi-Lite, which has the goal of promoting the use of formal methods in developing high-integrity software.
You can also view the presentation slides if you want to follow along.
Open-DO Update
View more presentations from AdaCore.
Also posted in Open-DO News, Papers and Slides Leave a comment