Category Archives: Events

Prove & Fly!

On December 5-6, I participated in the 2nd workshop on Theorem Proving in Certification, in Cambridge (UK). This turned out to be even more interesting than last year’s program promised.

The goal of the workshop is to clarify under which conditions theorem proving can be applied in the context of DO-178C Formal Methods Supplement (hence Prove & Fly!):

  • extent of verifications performed
  • cost/benefit compared to testing
  • characteristics of a technique/tool to be called theorem proving
  • tool qualification needs

The workshop was organized around a common challenge (gear nose challenge) which all participants were invited to address from different angles. The challenge was to compute the velocity of the nose gear of a plane while on the ground. This was made even more interesting by the need to comply with a small certification standard (Tamarack standard). Both the challenge and the certification standard were created by Jeff Joyce from CSL.

Besides sharing the strategy we follow in project Hi-Lite, and showing how it applied to the common challenge, I was very interested in the discussions we had over tool qualification and the alternate objectives to coverage in DO-178C, when using formal verification instead of testing. An interesting shared opinion was that the automatic prover does not need to be qualified if it generates a trace that can be double-checked independently by a theorem prover (based on a small set of induction rules). For example, that’s the case for CVC3. In the discussion on alternate objectives to coverage, Jeff Joyce clearly stated that the underlying goal is to detect incompleteness of specifications, or equivalently (from the opposite point of view) unintended functionalities. During the discussion, it appeared that we may be able to use either model checking to perform a symbolic coverage analysis, or information given by automatic provers stating which hypotheses (and thus source code constructs) were used in proofs, but for example not concolic testing which is based on source code.

Many of these subjects will need to be further explored as DO-178C is adopted in new projects and tools based on formal methods are applied in this context. In particular, I look forward to the evolutions of the Tamarack standard and new solutions to the gear nose challenge. Hot news: Open-DO will host the workshop forge and wiki to support these evolutions. :)

Also posted in Certification | Tagged , , | Leave a comment

Ada Connection 2011 – An Overview of DO-178C/ED-12C

From the Ada Connection 2011 talks, Dewi Daniels from Verocel gives an overview of DO-178C/ED-12C

Also posted in Videos | Leave a comment

Ada Connection 2011 – Real Time Longevity

From the Ada Connection 2011 talks, Frederic Pinot from Ansaldo STS talks about his experiences developing real-time systems for high-speed rail.

Also posted in Agile/Lean Programming, Videos | Leave a comment

Best Paper Award for Results of Verification Competition

Last year, the conference VSTTE 2010 organized a competition of software verification systems (language + tools), to improve understanding of each system’s pros and cons. Rod Chapman from Altran Praxis participated with the SPARK language and toolset, and solved the first problem even beyond what the subject asked. We have since provided solutions in SPARK to all five problems, like other teams, which formed the basis for a report that you can find on this page.

This report was deemed important enough by the organizers of the Formal Methods conference 2011 that they have granted it the best paper award.

Furthermore, the page of the competition contains an archive with all solutions in many different languages and systems… you can even DIY!

Also posted in Certification, Papers and Slides | 1 Comment

Real Time Linux Workshop 2011

The Real Time Linux Workshop 2011 will be held in Prague, October 20 to 22. The call for papers is now out with several topics of interest including “Safety-related FLOSS systems”. More details on the CFP and event can be found on the website:

https://www.osadl.org/RTLWS-2011.rtlws-2011.0.html

Posted in Events | Tagged | 1 Comment

PSP and TSP: Culture and Discipline for High-Assurance Software

From a talk given at the SPARK User Group 2010 High Assurance Software Symposium, Rod Chapman from Altan Praxis talks about the guiding principles behind PSP (Personal Software Process) and TSP (Team Software Process).



View more videos from the SPARK User Group
2010 High Assurance Software Symposium »

Also posted in Agile/Lean Programming, Videos | Leave a comment

Slides from the Couverture project conclusion meeting

Below are the slides from the recent Couverture project conclusion meeting. Cyrille Comar presented the original needs and goals of the project, the challenges the team came across a long the way, and the main results.
Also posted in Agile/Lean Programming, Certification, Open Source, Papers and Slides | Tagged , , , , , | Leave a comment

FLOSS for Safety-related Systems

At the upcoming Embedded World conference in Nuremberg, Germany, there will be a days conference on the use of freely-licensed open source software (FLOSS) to build safety-critical systems. Presentation topics include:

Validation of Linux for Safety-Related Systems
Linux as a real-time Hypervisor for the automotive industry
Efficient Safety Critical Systems Development – Is FLOSS the only answer?
Finding Misuses of Unsigned Integers in Linux Device Driver Code
“Open Proof” for Railway Safety Software A Potential Way-Out of Vendor Lock-in Advancing to Standardization, Transparency, and Software Security
Improved Redundancy and Consistency beyond RAID 1
Utilizing security methods of FLOSS GPOS for safety

A full program description can be found here.

Also posted in Open Source | Leave a comment

First TOPCASED Days 2011 conference

The first conference based around the TOPCASED toolkit project will take place in Toulouse February 2nd-4th, 2011.

TOPCASED (Toolkit in OPen-source for Critical Application and SystEms Development) is a modular, open-source, Eclipse-based software environment providing methods and tools for critical embedded systems development, ranging from system and architecture specifications to software and hardware implementation through equipment definition. TOPCASED promotes model-driven engineering and formal methods as key technologies.

Also posted in Certification, Related Initiatives | Leave a comment

SPARK Ada in High SIL Active Life Support (Alex Deas – Deep Life Ltd.)

From a talk given at the SPARK User Group 2010 High Assurance Software Symposium, Alex Deas from Deep Life talks about developing software for deep water rebreathers which must meet the rigorous European safety standard SIL3.
Also posted in Videos | 1 Comment
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org