Categories
Open-DO Projects
Contact
info @ open-do.org
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.
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!
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
Axioms and Proofs: When Less is More
In formal verification, we ultimately rely on automatic provers to decide whether formulas are valid (always true) or not. In GNATprove for example, we rely mostly on the ability of prover Alt-Ergo to analyze quickly the formulas we generate, and answer yes when the formula is valid or no when the formula is invalid (so there is a problem with the code or the assertions in the program). The reality is that the prover may take a long time to reply yes/no, and that in some cases it just replies I don’t know!
A promising approach to help automatic provers answer more quickly is to reduce the size of the formula. Typically, this formula contains thousands of axioms defining all relevant symbols from the program (functions, types, constants), as well as describing the context in which the formula should hold (typically a path or set of paths through a function, as produced by a verification condition generator). Researchers have proposed strategies to start with a small subset of these axioms, and incrementally grow it until a proof is found. At AdaCore, Duc Hoang is ending today a 6 months internship on that subject.
We have devised a strategy based on definition links, as in the work of Josef Urban (”An overview of methods for large-theory automated theorem proving”) and SInE, with a graph-based approach, similar to the work of Couchot et al. (”A graph-based strategy for the selection of hypotheses” & “Graph Based Reduction of Program Verification Conditions”).
This work is publicly available, if others want to try it out (main switch is -autoselect), in the git repository for our version of Alt-Ergo:
git clone https://forge.open-do.org/anonscm/git/alt-ergo/alt-ergo.git
We had a discussion a few days ago on this subject and others related to Alt-Ergo with CEA-LIST research lab and OCamlPro company, both interested in a shared development of Alt-Ergo. If you are also interested in joining this effort, contact us at AdaCore.
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.