I was invited today to give a talk at Fraunhofer FIRST, a German research institute, on Formal Verification in Aeronautics: Current Practice and Upcoming Standard. I told them about the pioneering work done at Airbus, especially related to unit proof to replace unit testing, and about the new version of the DO-178 standard (the ‘C’ version) expected in 2011, which states that formal methods can be used instead of testing.
Contrast what the DO-178B says:
Formal methods are complementary to testing.
to what the (draft of the) DO-178C says:
Formal methods [...] might be the primary source of evidence for the satisfaction of many of the objectives concerned with development and verification
The audience was around 15 people, half of which from the railway industry in Germany, Belgium and Italy. Their reason for coming to this two-day tutorial around the tool Frama-C, developed by CEA LIST and used at Airbus, is that they have watched with increasing interest the advances of formal methods in the avionics industry, and they would like to apply some of it to the railway domain when possible. Very encouraging, and thanks Jens Gerlach from Fraunhofer FIRST for organizing this kind of events!
2 Comments
Formal methods are already heavily used in the railway industry. Siemens, Alstom and Areva are all using the B Method to develop their driverless subway systems.
However, this is true that current standards in railway do not acknowledge formal methods as the “the primary source of evidence” for verification. Currently formal methods are only “Highly Recommended”. The evolution of DO-178 from revision B to C is interesting in that regards.
Heavily used yes, but heavy formal methods too.
What I mean is that using the B method does not integrate easily with a regular process of coding manually other parts of an application, if the two parts cannot be separated clearly. This is what are called usually the ‘heavyweight formal methods’.
What we want to push in Hi-Lite is ‘lightweight formal methods’ where you can analyze formally parts of the code and do testing for other parts.
Heavyweight formal methods will always provide more guarantees than lightweight formal methods, because you can enforce them on all the code, but they require more efforts from those willing to apply them.
None of the people from railway industry which was present at the Fraunhofer workshop was in a company using the B method for example.