Category Archives: Certification

Interesting new UK conference

HIS 2014 is announced as “the UK conference for sharing information about the key challenges and recent developments in high integrity software engineering. This one day conference will be held in Bristol, UK on 23rd October 2014 and will feature presentations on current industrial experience as well as keynote talks from leading industry experts.”

An interesting program includes keynotes from Martyn Thomas and Harold Thimbleby and a number of international speakers. The talks are grouped into four main sessions:

    - Software Security
    - Software Safety
    - Applications
    - Languages and Technologies

More info and registration.

Also posted in Events | Leave a comment

Parallel Programming Languages Enable Safer Systems

Languages that use garbage collection pose tricky issues for military system developers. In this recent article COTS journal article, Tucker Taft looks at innovative new parallel programming techniques that offer a safer solution.

http://www.cotsjournalonline.com/articles/view/104120
Posted in Certification | Leave a comment

ERTS 2014: Integrated and Simpler Systems

I attended last week the 7th edition of the congress on Embedded Real Time Software and Systems that takes place in Toulouse (France) every two years. It started with Joseph Sifakis inviting all of us to work on the integration of embedded systems with Internet, and the Engineering Executive Vice-President of Airbus, Charles Champion, describing the many future challenges of avionics and asking, maybe surprisingly, for simpler software and systems to meet these challenges.

At the software level, I see two important trends contributing to these goals: model-based development and formal methods. The former because it facilitates communication between systems and software engineers, at the right level of abstraction, the latter because it makes the verification of these ever larger and integrated systems tractable thanks to abstraction and automation. No surprise then that both were very much present in presentations at the conference. A difference with previous years was that many of these presentations were backed by large industrial case studies. For example, for model-based development, the use of MBD in the context of DO-178C at Airbus Military, and for formal methods, the use of Event-B for requirements verification at BAE Submarine. The most interesting trend for me was the combination of model-based development and formal methods to manage greater integration between systems. We described such a workflow in our paper on System to Software Integrity. I expect more of these in the next edition.

Another highlight of this conference for me was certification, with two sessions dedicated to New Trends in Certification, among which a majority of papers on formal methods (5 papers). It will be interesting in the years to come to follow progress on the convergence of certification domains on the issues of tool qualification and formal methods.

Also posted in Events | Leave a comment

Safe and Secure Software – An Invitation to Ada 2012

The aim of this booklet is to show how the study of Ada in general, and the features introduced by Ada 2005 and Ada 2012 in particular, can help anyone designing safe and secure software regardless of the programming language in which the software is eventually written. After all, successful implementers of safe and secure software write in the spirit of Ada in any language!

To download the booklet, please visit this page.

Also posted in Papers and Slides | Leave a comment

not Taking Assumptions for Granted

The Merriam-Webster dictionnary defines an assumption as “a fact or statement (as a proposition, axiom, postulate, or notion) taken for granted”. This is indeed the role that assumptions play in formal verification of programs, as performed in Frama-C platform or GNATprove. Assumptions may either be related to the proof of a single function (like “this other function called should respect its contract”) or related to the proof methodology and tools used (like “the type system of the program should not be bypassed”). The problem is that the overall verification of a software, as done in certification, should ultimately discharge such assumptions, either by some other automatic verification activity, or by manual review. Because assumptions are not taken for granted in software certification.

Researchers have started taking assumptions seriously, in particular for certification. See for example this paper at FM 2012, and the paper “Tool Integration with the Evidential Tool Bus” (or ETB) from SRI. The Frama-C platform already has a built-in mechanism for storing the assumptions on which individual proofs of properties depend (see their paper “Combining Analyses for C Program Verification”). The SPARK technology also provides a way to summarize how all properties of interest were checked, inclusing manual review, so that there are no pending assumptions besides the implicit ones depending on the approach.

What we have been discussing last Monday with Simon Cruanes (a coauthor of the SRI paper above) and Frama-C team members Julien Signoles and Virgile Prevosto, is how to combine verification results from different tools (some doing formal verification, some doing dynamic verification like testing) on different languages (Ada and C) in a way that no assumption is forgotten. The Datalog language used to express constraints in the ETB seems a good start. We are now going to experiment with the ETB and its Datalog language to see if that allows us to express and check the verification constraints mandated by various certification standards, for our tools.

Note that the CEA will host soon Maria Christakis (a coauthor of the FM 2012 paper above) and SRI researchers Natarajan Shankar and Sam Owre, which whom we’ll discuss this topic. To be continued.

Posted in Certification | Tagged , , , | Leave a comment

DO-178C/ED-12C vs DO-178B/ED-12B: Changes and Improvements

This document identifies all the changes in the new release DO-178C/ED-12C, explains their rationale, and highlights the impact of these changes on the various software processes. The PDF can be downloaded here.

© Frédéric Pothon, 2012
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License.

Also posted in Papers and Slides | Leave a comment

Use of formal methods in critical systems conference

This conference will take place in Toulouse on November the 12th. It is in French as is the announcement providing more details below:

Les animateurs du DAS Systèmes Embarqués, avec le soutien du thème IFSE du RTRA AE/SE, ont le plaisir de vous annoncer la programmation d’un cycle de conférences techniques sur les méthodes formelles de développement. Non, ne partez pas tout de suite : les méthodes formelles sont faites pour vous !

Ces méthodes ne sont pas assez connues mais ont un potentiel énorme pour faire progresser la productivité ET la qualité intrinsèque des développements de logiciels embarqués et de leurs outils de développement et de vérification. Et elles ne sont pas si difficiles à mettre en Å“uvre : certains l’ont déjà fait, avec succès, pourquoi pas vous ?

Nous vous proposons donc un cycle de conférence/forum pour vous présenter bien sûr les fondements théoriques de ces méthodes, mais surtout faire un état de l’art et de la pratique, démystifier, échanger, et pourquoi pas monter ensemble des projets pour “passer à l’acte” ? Les intervenants seront à la fois des scientifiques et universitaires les plus compétents dans ces domaines et des utilisateurs “de terrain” qui ont déjà pratiqué ces méthodes et vous livreront leurs retours d’expérience.

La première conférence de ce cycle aura lieu le mardi 13 Novembre 2012 à l’IAS, 23 Avenue Edouard Belin, Toulouse, sur le thème de “l’Utilisation des méthodes formelles dans les systèmes critiques”.

Read More »
Also posted in Events | Tagged , , | Leave a comment

Safe and reliable embedded linux programming

Dr José Ruiz gave this talk at yesterday’s Embed with Linux conference in Lorient, France. The talk provides an overview of techniques to design and implement reliable embedded applications. The goal is to achieve safe and analyzable behavior by construction, including handling parallel multiprocessor systems in an efficient and predictable way. The means to attain this objective is to statically configure the application to run on embedded linux platforms, and then to use run-time support to enforce constraints imposed to the system.

Also posted in Events, Papers and Slides | Leave a comment

Excellent paper on avionics software certification

John Rushby from the SRI International Computer Science Library has written a very interesting paper considering the “New Challenges In Certification For Aircraft Software”.

Abstract:

We outline the current approach to certification of aircraft software, and the role of the DO-178B guidelines. We consider evidence for its effectiveness and discuss possible explanations for this. We then describe how changes in aircraft systems and in the air traffic system pose new challenges for certification, chiefly by increasing the extent of interaction and integration.

The full paper can be found at http://www.csl.sri.com/users/rushby/papers/emsoft11.pdf
Posted in Certification | 1 Comment

Formalization and Comparison of MCDC and Object Branch Coverage Criteria

This paper was presented by Jerome Guitton at the recent ERTS 2012 conference:
This paper presents formal results derived from the COUVERTURE project, whose goal was to develop tools to support structural coverage analysis of unin- strumented safety-critical software. After briefly introducing the project context and explaining the need for formal foundations, we focus on the relationships between machine branch coverage and the DO-178B Modified Condition/Decision Coverage (MCDC) criterion. A thorough understanding of those relationships is important, since it provides the foundation for knowing where efficient execution trace techniques can be used to demonstrate compliance with the MCDC criterion. We first present several conjectures that were tested using Alloy models, then provide a formally verified characterization of the situations when coverage of object control-flow edges implies MCDC compliance.The full paper can de downloaded here.

Also posted in Open Source, Open-DO News, Papers and Slides | Leave a comment
  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org