Category Archives: Open-DO News

Dissimilar tools: Use cases and impact on tool qualification level

Frequently, the lack of existing qualifiable COTS tools raises the question whether two separately developed and thus dissimilar tools that satisfy the same operational requirements may be used instead of a single tool, either to avoid the need for qualifying that tool or to serve as an alternative method for tool qualification.

This question may be answered in different ways by different certification authorities, since no guidance or guidelines are provided in the applicable standards, such as DO-178C/ED-12C. DO-330/ED-215 identifies the use of dissimilar tools as an example of “alternative method for tool qualification” but without definition of the actual impact of such approach. DO we have to understand that the use of non-qualified dissimilar tools replaces the need for qualification of a single tool? Is this applicable for all TQL?

This paper presents several use cases based on the type of tools and certification credit, and examines the possible impact on the need for qualification and the applicable Tool Qualification Level of the use of dissimilar tools.

Disclaimer: Discussion of this topic in the Forum for Aeronautical Software (FAS) raised controversial questions and different opinions. Therefore, it was difficult to reach a consensus on an Information Paper. It was decided that this topic is beyond the scope of the FAS working group, and the proposal was withdrawn. This document reflects the author’s point of view, based on his background and experience. It should help readers to provide an acceptable rationale for a software life cycle using dissimilar tools in place of a single qualified tool.

The author, Frédéric Pothon ACG Solutions, and several of the contributors and reviewers participated in the DO-178C/ED-12C working group and subcommittees.

Download Document

© Frédéric Pothon, 2015

This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License.

Posted in Open-DO News | 11 Comments

How to prevent drone crashes using SPARK

I recently joined AdaCore as a Software Engineer intern. The subject of this internship is to rewrite a drone firmware written in C into SPARK.

Some of you may be drone addicts and already know the Crazyflie, a tiny drone whose first version has been released by Bitcraze company in 2013. But for all of those who don’t know anything about this project, or about drones in general, let’s do a brief presentation.

The Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly available on their GitHub and its architecture is very flexible. These two particularities allow the owner to add new features in an easy way. Moreover, a wiki and a forum have been made for this purpose, making emerge a little but very enthusiastic Crazyflie community!

Now that we know a little more about the Crazyflie, let me do a brief presentation of SPARK and show you the advantages of using it for drone-related software.

Even if the Crazyflie flies out of the box, it has not been developed with safety in mind: in case of crash, its size, its weight and its plastic propellers won’t hurt anyone!

But what if the propellers were made of carbon fiber, and shaped like razor blades to increase the drone’s performance? In theses circumstances, a bug in the flight control system could lead to dramatic events.

SPARK is an Ada subset used for high reliability software. SPARK allows proving absence of runtime errors (overflows, reading of uninitialized variables…) and specification compliance of your program by using functional contracts.

The advantages of SPARK for drone-related software are obvious: by using SPARK, you can ensure that no runtime errors can occur when the drone is flying. Then, if the drone crashes, you can only blame the pilot!

After this little overview, let’s see how we can use SPARK on this kind of code.

See more at: http://blog.adacore.com/how-to-prevent-drone-crashes-using-spark

Posted in Open-DO News | 6 Comments

Project P Open Workshop

Project-P Open Workshop
Model-driven engineering and qualifiable code generator

http://www.open-do.org/projects/p/

Project P is a three-year research project funded within the French FUI 2011 funding framework. It sees the collaboration of major industrial partners (Airbus, Astrium, Continental, Rockwell Collins, Safran, Thales), SMEs (AdaCore, Altair, Scilab Enterprise, STI), service companies (ACG, Aboard Engineering, Atos Origins) and research centers (CNRS, ENPC, INRIA, ONERA).

With the project now drawing to an end comes the final presentation of all the work that has been produced over the past 3 years…

Continental France, Project P leader, and all the project partners are pleased to invite you to the presentation of the final results of Project P.

The event will take place on Tuesday 16th June 2015 from 1:30pm to 5:30pm at Pôle Systematic – Palaiseau, Amphitheatre building N°3 – Nano-Innov

To find out more about access, please click here: http://www.systematic-paris-region.org/sites/default/files/Plan%20Nano%20INNOV2.pdf

Agenda

1:45pm – 2:00pm: Welcome

2:00pm – 4:00pm : Presentations

    Introduction to Project-P (Continental)
    Development and qualification of a generic code generation framework (ACGs)
    QGen: a qualifiable code generator for Simulink/Stateflow models (AdaCore)
    Operational use of a code generator (Sagem and Thales Alenia Space)
    Overview of other generators used in the project (AdaCore)
    A code generator for UML models (ATOS Origin)
    A formal verification perspective (IRIT)

4:00pm – 5:30pm : Workshop Demonstrations

    Model Verification and Code Generation with QGen (AdaCore)
    Hardware code generation with GAUT (LabSticc)
    Software code generation for XCOS models (Scilab Enterprise)
    Code generation from NSP language and Scicos (Inria/Altair/ENPC)
    Multi-formalism (UML and Simulink) code generation (ATOS/AdaCore)
    Generated code interoperability and schedulability analysis with SynDEx (INRIA)
    Verification of formal requirements for generated code (IRIT, ONERA)
    Description of formal requirements for generated code  (IRIT)

Registration is mandatory and closes on June 10th 2015 …to do so, please contact s.minault@systematic-paris-region.org.

Philippe CUENOT
Continental Automotive France
Tel : 05-61-19-88-88
philippe.cuenot@continental-corporation.com

Posted in Open-DO News | Leave a comment

SPARK Formal

The SPARK Formal project aims to develop a complete set of semantics of the SPARK language in Coq, for:

    - at the language level, ensuring the absence of ambiguity and the completeness of evaluation rules
    - at the tool level, ensuring the correct insertion of checks in the AST used for compilation and analysis

The formalization of SPARK also paves the way for the creation of proved toolchains for SPARK programs (a.k.a. “certified” toolchains in academia) such as CompCert.

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

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 , , | 5 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

SPARK 2014 – Future directions

Stuart Mathews gave this talk at the recent SPARK User Group. In it he presents the next generation of the SPARK language which will extend the range of programs that can be automatically verified and provides an innovative means for combing formal verification and testing.

Posted in Open-DO News | Leave a comment

Directions in Secure Software Development

Rod Chapman, Altran Praxis, gave this talk at the recent SPARK User Group. This talk reflected on our experiences with building secure systems with SPARK and other formal methods, including the lessons learned from the MULTOS CA, Tokeneer and SPARKSkein projects, and the relationship between safety- and security-critical development. In recent years, there has been a huge resurgence in interest in static analysis of software, largely driven by the perception of “security vulnerabilities” in both specific systems and programming languages in general. This talk also considered the trends emerging in this market, both good and bad, and proposed one view of what the future might hold for secure systems development.

Posted in Open-DO News | Leave a comment
  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org