If you read a bit of French, you’ll be happy to know that Hermes Publishing has just issued the first of a three-volume series on
Utilisations industrielles des techniques formelles (use of formal methods in industry). This first volume is concerned with abstract interpretation techniques and tools.
As such, we at AdaCore contributed a chapter on the static analyzer CodePeer that we develop. Other chapters describe the use of other tools based on abstract interpretation and
formal methods in a broader sense: Polyspace, Astrée, Frama-C, etc. I liked in particular the discussion about the use of formal methods for in DO-178C context, and the combination of
formal verification and testing, in chapter 7 by Dassault Aviation Méthodes formelles et conformité au standard DO-178C/ED-12C en aéronautique. We do have solutions in project Hi-Lite to
some of the problems they raised.
Here is the book, that you can also find at your preferred web merchant.
The two remaining books on the B methods, Scade, SPARK and others, should be published by the end of 2011. An English version of the three books is expected to be published in 2012.
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!
In case you do not know the series of books “for Dummies”, its principle is
to explore a subject from the ground up, with rich explanations and examples
for non-experts. That’s in my view a valid alternative title for the recently
published “Guidance to Avoiding Vulnerabilities in Programming Languages
through Language Selection and Use”. Rich (around
70 vulnerabilities explored) + detailed (130 pages!) + accessible (it contains
the best discussion I’ve read of unspecified/implementation-defined/undefined
behavior).
The ISO/IEC committee has produced here a language-neutral evaluation of the
ways in which a language may “come in the way”, and how to avoid traps and
pitfalls either upfront (in language design) or in the field (through coding
standards and use of static analysis tools). This is a must-read for anyone
whose task is to establish coding guidelines, recommend the usage of a static
analysis tool, or choose a programming language for some project.
While Ada and SPARK naturally stand as the languages with fewer
vulnerabilities, it also shows the many uses of static analysis tools, from
coding standard checking (like GNATcheck) to static analysis (like CodePeer)
and formal proof (like SPARK toolset). The recommendations also match well the
restrictions for the Alfa subset of Ada that we are defining in project
Hi-Lite. (See for example the discussion of aliasing in section 6.39 “Passing
Parameters and Return Values”.)
The open source coverage analysis tool
GNATcoverage issued from the
Couverture Project was awarded with an Electrons d’Or from the
Electroniques magazine. GNATcoverage won the prize for the Software Tool category in a prize-giving ceremony in Paris.
In a recent article in Electronic Design, Ben Brosgol discusses with Bill Wong about safety and security concerns in medical device software and how “recent Food and Drug Administration (FDA) regulations are dealing with such issues, and how programming language and support tool technology can help”
The full article can be found at:
http://electronicdesign.com/article/embedded/Safety-in-Medical-Device-Software-Questions-and-Answers.aspx
A recently published paper by the National Institute of Standards and Technology (NIST), examines software assurance tools as a fundamental resource to improve quality in today’s software applications. It looks at the behavior of one class of software assurance tool: the source code security analyzer. Because many software security weaknesses are introduced at the implementation phase, using a source code security analyzer should help reduce the number of security vulnerabilities in software.
The report – Source Code Security Analysis Tool Functional Specification Version 1.1 (NIST Special Publication 500-268 v1.1) – defines a minimum capability to help software professionals understand how a tool can help meet their software security assurance needs. The example languages studied are C, C++, Java and SPARK. The NIST report identifies the languages’ vulnerabilities. As you would expect, the SPARK language comes out well.
We have posted a new paper to the Open-DO website “High-Integrity Object-Oriented Programming in Ada“. This paper’s goal is to provide guidance on how to use Ada’s Object Oriented (OO) features for High-Integrity applications; i.e. high-reliability systems with requirements for safety and/or security which may need to demonstrate compliance with domain-specific certification standards. The paper’s authors have extensive experience in this area through their participation in industrial working groups such asthe joint EUROCAE WG71 / RTCA SC 205 working group defining the upcoming RTCA DO178-C/EUROCAE ED12-C avionics safety standard, and ISO’s Ada Rapporteur Group that manages the Ada language standardization process. More information can be found at http://www.open-do.org/high-integrity-oo-programming-in-ada/
We expect this document to evolve over time, so we kindly ask readers to provide as much feedback as possible to AdaCore at info@open-do.org with the name of the document mentioned on the subject line.
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 real time linux |
We learned this week of ImProve, a lightweight DSL intended for building high assurance embedded applications. Developed by Tom Hawkins, the tool is an EDSL that performs formal verification (via. model checking) and code generation. The host language is Haskell; meaning ImProve programs are nothing more than Haskell programs that call the ImProve library API.
ImProve’s semantics are extremely simple:
- It is an imperative language like C or Ada.
- It only has 3 datatypes (bool, int, float).
- There are a total of 16 expression types (add, subtract, AND, OR, etc.).
- Statements consist of variables assignments, conditional “IF” statements, and assertions.
In terms of the ImProve compiler structure, a thin layer of Haskell helps translate ImProve programs down to an intermediate representation, from which programs are verified and C code is generated.
For verification, the IR language is passed to a k-induction model checker (part of the ImProve library), which makes calls down to an SMT solver (currently Yices). ImProve provides assertions statements to capture design intent. Assertions can be seeded with previously proven lemmas to aid verification convergence.
For more information, please visit the project website:
https://github.com/tomahawkins/improve/wiki/ImProve
A number of very interesting articles in February’s SoftwareTech News look at the use of FLOSS by the DoD. Topics below give an insight the DoD’s position and strategy in employing open source software.
Software is a Renewable Military Resource
Military Open Source Community Growing
Evaluating Open Source Software
Open Source Software Is Commercial
Implementing Open Standards in Open Source
Running Open Technology Development Projects
Publicly Releasing Open Source Software Developed for the U.S. Government