Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do.
Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification objectives that this use of formal methods allows to reach, and how this is obtained and documented. In order to facilitate this process, the participants to the workshop on Theorem Proving in Certification have produced a draft set of guidelines, now publicly available.
My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.
The University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been proved free from run-time errors. This project is part of the secure multilevel workstation project by Secunet, a German security company, which is using SPARK and Isabelle to create the next generation of secure workstations providing different levels of security to government employees and military personnel. I present why I think this project is worth following closely.
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.
This conference will take place in Toulouse on November the 12th. It is in French as is the announcement providing more details.
This is the paper that Yannick Moy presented at the recent ERTS 2012 conference: Verification activities mandated for critical software are essential to achieve the required level of confidence expected in life-critical or business-critical software.
The DO-333 is now available! (ok, that’s not free: 215$ for an electronic version, or 300$ for a hard copy, pfew!)
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.
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.