People from the group developing Spec# at Microsoft Research finally published an article on their new Code Contracts approach.
Chosen excerpts: “embedding of contracts as code is a better approach”; “The language of conditions is just the language of expressions
in the programming language used”; “ForAll and Exists that work over integer ranges and collections”; “Any methods called from within contract expressions
should be pure methods”; “Runtime contract checking is particularly
eff ective in conjunction with automated testing”; “generating good documentation from the embedded
contracts is a key scenario”.
And the conclusion: “Since contract expressions are compiled by the existing
compiler, the typical problem of having the speci cations
and the code drift apart due to edits, refactoring, etc., is
avoided.”
All of this supports the vision of project Hi-Lite, and provides valuable experience reports which should inspire us in Hi-Lite.
It presents the Couverture approach to object and structural coverage analysis for certified safety-critical applications, in particular in the context of DO-178.
The next talk in our series from the recent Open-DO Conference is from Hervé Delseny, an expert in Avionics Software Aspects of Certification at Airbus. In his talk he gives examples of Airbus’ use of Formal Methods to verify avionics software, and summarises the integration of Formal Methods in the upcoming ED-12/DO-178 issue C.
You can also view the presentation slides if you want to follow along.
The next talk in our series from the recent Open-DO Conference is from Neil White, Principal Engineer with Altran Praxis. His talk provides an overview of the formal methods used on the iFACTS project. iFACTS is delivering increased Air Traffic Control capability to the UK.
You can also view the presentation slides if you want to follow along.
The next talk in our series from the recent Open-DO Conference is from Dr. Peter Gardner. Peter has twenty years experience in languages and software development methodologies and acts as the focal point for UML in Silver Atena. His talk surveys Agile methods and formulates a list of features that occur in these methods, then considers whether each of the features can be applied in the field of safety-critical software development.
You can also view the presentation slides if you want to follow along.
The next talk in our series from the recent Open-DO Conference is from Cyrille Comar, Managing Director of AdaCore EU, who gives an update on the latest happenings with the Open-DO initiative and talks about AdaCore’s new French government funded project, Hi-Lite, which has the goal of promoting the use of formal methods in developing high-integrity software.
You can also view the presentation slides if you want to follow along.
Couverture is a qualifiable tool to measure structural coverage. This paper describes how the Couverture technology copes with the “Souce Code VS Object Code Coverage” debate in a DO-178 context.
The Couverture project is hosted on the Open-DO Forge.
The attached paper is also published in the Ada User Journal, December 2009 issue.
Last week I attented the Grenoble (October 20, 2009) and Valence (October 22, 2009) conferences as part of the Agile Tour 2009 series. These events were a big success and attracted more than 450 attendees! I would like to thank one more time the CARA who did a very good job at organizing these.
The presentations were of very high quality and their diversity pleased practionners as well as managers and students. All the slides are accessible on the CARA’s website (French and English).
I gave a talk in Grenoble and Valence about the infrastructure and processes we put in place at AdaCore to build and test on a daily basis all our compilation chains and accompanying technology in a Lean fashion.
I also presented the “qualification machine” we have built based on open source technology to ease the DO-178B tool qualification process by adopting an agile philosophy.
Cyrille Comar gave a talk at the recent SAFECOMP conference on the work being undertaken by the SC-205 and WG-71 working group on the upcoming DO-178C standard. He gives particular attention to the Tools Qualification Supplement, the OOT (Object-Oriented Technology) Supplement, and the Formal Methods Supplement.