Category Archives: Related Initiatives

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.
Also posted in Open Source | Leave a comment

GNATprove tool available

We are happy to announce the first release of GNATprove. This tool is used for formal verification of Ada programs and is being developed as part of the Hi-Lite project. We provide binary distributions for x86 linux, x86 windows and x86-64 bit linux. More details can be found on the following page:

http://www.open-do.org/projects/hi-lite/gnatprove/

For questions, remarks, or issues please contact us on hi-lite-discuss@lists.forge.open-do.org

Posted in Related Initiatives | 5 Comments

ESA is Funding Students on Open-Source Projects this Summer

The European Space Agency is reediting its SOCIS initiative this year. Open-source projects can submit proposals, and ESA will fund between 20 and 25 students to work during two months on these projects.

We submitted a project to extend our work on standard containers adapted to formal verification. Submit yours by July 15th!

Also posted in Open Source | Leave a comment

Hi-Lite team paper at FM 2012

The 18th edition of the International Symposium on Formal Methods organized by Formal Methods Europe will take place at the CNAM in Paris this August. A paper on the work being undertaken by the Hi-Lite team on “Maximal and Compositional Pattern-Based Loop Invariants” will be presented there.

Below is the abstract:

“We present a novel approach for the automatic generation of inductive loop invariants over loops manipulating arrays. Unlike most existing approaches, it generates invariants containing disjunctions and quantifiers, which are rich enough for proving functional properties over programs which manipulate arrays. Our approach does not require the user to provide initial assertions or postconditions. It proceeds by recognizing through static analysis simple code patterns that respect stability properties on accessed locations, on an intermediate representation of parallel assignments. We associate with each pattern a formula that we prove to be a so-called local invariant, and we give conditions for local invariants to compose an inductive invariant of the complete loop. We also give conditions over invariants to be locally maximal, and we show that some of our pattern invariants are indeed maximal.”

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

Nose Gear Challenge Problem joins Open-DO

The Nose Gear Challenge Problem has joined the Open-DO forge. It was initially developed to stimulate and unify discussions at the 2nd Workshop on Theorem Proving in Certification held on December 5 – 6, 2011 in Cambridge, UK. The goal of this project is to consider how/if theorem proving can have any value in providing assurance in the context of DO-178C formal method supplement. The contributors to the project can use the Nose Gear problem example to explain their techniques.

Visit the Nose Gear Challenge Problem project page on the Open-DO forge.

Also posted in Certification, Open Source | 1 Comment

Executable Annotations for C Programs

The Frama-C platform, which integrates static analysis and formal proof of C programs, now has a plug-in for run-time execution of annotations. In particular, preconditions and postconditions written using the E-ACSL subset of the ACSL annotation language for C can now be executed thanks to this plug-in. This is a great move in the direction of better integration of proofs and tests for C programs!

As far as I know, this is the first attempt at defining a common annotation language for tests and static analysis / proof for C. The annotation languages for C that I know of cannot be executed: Microsoft’s widely used Standard Annotation Language, the annotation language used by the Escher C Verifier or the one from Microsoft’s VCC.

Note that an important difference between this annotation language and others is that it uses mathematical semantics for operations in annotations. So an addition in annotations cannot overflow. In practice, they are using the GMP library for mathematical integers. Try it for yourself by downloading/installing Frama-C and this plug-in!

Also posted in Open-DO News | Tagged , | Leave a comment

code.NASA

An interesting new website added to the family of NASA websites. code.NASA, according the website, NASA “…will continue, unify, and expand NASA’s open source activities. The site will serve to surface existing projects, provide a forum for discussing projects and processes, and guide internal and external groups in open development, release, and contribution.”

More information can be found at:

http://open.nasa.gov/blog/2012/01/04/the-plan-for-code/

I particularly like the call for participation – “Will your code someday escape our solar system or land on an alien planet? We’re working to make it happen, and with your help, it will.”

Also posted in In the Press, Open Source, Open-DO News | 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, Events | Leave a comment

Safety-critical software and formal verification

Below are a couple of links to a paper and an article discussing the formal verification of safety-critical applications.

The first one is an article written by Boris Sedacca in the IET magazine “Verifying safety-critical aerospace and automotive applications” looking at how the current and upcoming Avionics and Automotive standards “aim to improve code verification”.
http://kn.theiet.org/magazine/issues/1013/verifying-safety-1013.cfm

The second one is a paper written by Xavier Leroy who is a member of the team at INRIA working on the CompCert project. “The paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness.”
http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf

Also posted in Certification | Leave a comment

Certification Together Conference

According to the website, “The Certification Together International Conference for the Aeronautical Industry is the only event in Europe fully dedicated to System, Software and Hardware certification challenges.”

Looking at the program, a large part of it, as you’d expect, is dedicated to the changes in the upcoming DO-178C standard and how it will affect current certification process and practices. Coupled with these are more practical, hand-on user studies provided by primes and vendors alike.

Cyrille Comar will be giving a talk based around “The challenges of Agile certification” and an update on the Object Oriented Technology (OOT) supplement of DO-178C.

The event will be held in Toulouse, France – Oct 26-28.

Also posted in Agile/Lean Programming, Certification, Events | Leave a comment
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org