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.

Posted in Certification, Events | 1 Comment

Software Glitches: Why We Shouldn’t Put Up With Them

Robert Dewar discusses why software glitches are unacceptable in this day and age.

Software Glitches: Why We Shouldn’t Put Up With Them
Posted in In the Press | Leave a comment

Muen Separation Kernel

The Institute for Internet Technologies and Applications at the University of Applied Science in Rapperswil (Switzerland) and AdaCore today announced a significant expansion of the Open Source software model into the domain of high-assurance systems with the preview release of the Muen Separation Kernel. The Muen Kernel enforces a strict and robust isolation of components to shield security-critical functions from vulnerable software running on the same physical system. To achieve the necessary level of trustworthiness, the Muen team used the SPARK language and toolset to formally prove the absence of run-time errors.


More info.
Posted in Open Source, Related Initiatives | Leave a comment

Trusted Key Manager for IKEv2

The HSR University of Applied Sciences in Switzerland has implemented the TKM from scratch using the Ada programming language. The new Design-by-Contract feature of Ada 2012 has been used for the implementation of state machines, to augment the confidence of operation according to the specification. The TKM works in conjunction with the strongSwan IKEv2 daemon to provide key management services for IPsec.

Read the project report http://www.codelabs.ch/tkm/ike-separation.pdf
Visit the TKM project page http://www.codelabs.ch/tkm/
Visit the strongSwan project page http://www.strongswan.org/
Posted in Open Source | Leave a comment

Sparkel Programming Language

Sparkel is a new parallel programming language inspired by the SPARK subset of Ada, and designed to support the development of inherently safe and secure, highly parallel applications that can be mapped to multicore, manycore, heterogeneous, or distributed architectures.

To learn more about Sparkel and to follow the project, please visit http://www.sparkel.org
Posted in Open-DO News | Leave a comment

Ada for the C++ or Java Developer

This document will present the Ada language using terminology and examples that are familiar to developers that understand the C++ or Java languages.

To download the booklet, please visit this page

Posted in Open-DO News | 1 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.

Posted in Certification, Papers and Slides | Leave a comment

Using Formal Verification in the Landing Field

An article which I co-authored was just published in the May-June special issue of IEEE Software on Safety-Critical Software. It’s called Testing or Formal Verification: DO-178C Alternatives and Industrial Experience, and it talks about how to use formal verification instead of testing for software in civilian airplanes (for which DO-178C applies). It is based on the experience of Airbus and Dassault-Aviation in the application of formal verification with the Frama-C platform.

We describe:

  • What the avionics certification standard DO-178C asks in replacement for test coverage, which does not apply when one uses formal verification instead of testing.
  • How formal verification tools can help with these alternate objectives.
  • The solutions that Airbus and Dassault-Aviation have implemented to cover these objectives.

We’ll be happy to get some feedback from others! Please comment. This paper is copyrighted by IEEE, and reproduced here with their permission. You can also access it on IEEE Software website.

Posted in Papers and Slides | Tagged , | 1 Comment

GNATprove Takes the Train

David Mentré from Mitsubishi Electric R&D Centre Europe has produced a very interesting report on his use of GNATprove (the formal verification tool we develop for the next version of SPARK) on a case-study from the Open-ETCS European project, to develop the tools for the future European Train Control Systems.

Although David asked me to mention this is highly experimental (neither fully proved nor fully tested), I think it shows quite well what one can do with formal verification. The report contains inlined code showing how some units were specified using preconditions/postconditions and annotated with assertions for proofs. You can also download the code from github, or browse it online.

David will present this model at an internal Open-ETCS meeting next Monday, I’ll ask him to post the conclusion of his presentation!

Posted in Open-DO News | Tagged , , | 2 Comments

Integrating Proof and Testing in Verification Strategies for Safety Critical Systems

This talk was given by Cyrille Comar at the recent SPARK User Group. This talk reviews the prominent place and role testing holds in Safety Standards. It compares the strengths and weaknesses of testing with an alternative verification technique based on formal methods. It then explores specific instances where a combination of both approaches makes sense and can bring significant cost savings, without forcing dramatic changes in internal development procedures.

Posted in Open-DO News | 2 Comments
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org