Following the inaugural event last year, the 2nd International Workshop on Formal Methods and Agile Methods is taking place in Pisa, Italy, September 17 2010.
According to the website, “the aim of this workshop is to seek and to discuss novel ideas about combining FM and AM in the domain of software development, with the goal of making formally sound development methods faster, and rapid methods of development more formally sound. This goal could be approached in various different ways, for example by providing tool support to an ‘agile’ software development group, or by adopting ‘agile’ practices such as pair work into the domain of formal modelling.”
More information can be found at http://fm-am-2010.tripod.com/index.html
We are pleased to welcome the HiberSource project to Open-DO. This configuration management system is used to manage project data in accordance with DO-178B and supports the full software life cycle.
There are many free version control systems (such as SVN) but there are no free configuration systems to support projects (like Razor or PVCS). HiberSource was started to be a configuration system to support full software life cycle with developing, verification and other certification activities.
For more information, please visit the project on the Open-DO forge.
Last month I attended part of the Formal Methods Week 2009 in Eindhoven. Each year the FMWeek brings the world of formal verification together, with an emphasis on academic and industrial partnerships.
Although I am familiar with the field, I was still impressed by what is currently possible with tools based on formal methods. Although it will never be 100% automated, you can already get very strong guarantees on industrial products with high levels of automation.
Two examples show it better:
Airbus presented their use of formal verification tools for DO-178B software. Five of the six tools that were presented are in use within operational units. This presentation echoed, 10 years later, the presentation they gave at FM 1999 about their first trial with formal verification. With a decade of experience in industrial use of such tools, they have defined 5 “must-have” criteria: soundness, applicability to the code, usability by “normal” engineers on “normal” computers, improve on classical methods, certifiability. Very important lessons indeed.
André Platzer from CMU presented his work on formal verification of flight collision avoidance maneuvers which won the best paper award. This is quite a leap in coverage of formal methods: verifying nonlinear properties involving curves, differential equations etc. with almost complete automation.
Just to give you a flavor of it:
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.