Formal Methods
In a safety critical system, where correctness is vital, it is infeasible to rely on testing. The number of tests needed to prove correctness within required limits can be astronomical.
Formal methods offer us a development strategy which can significantly reduce the number of errors in our final system. According to Holloway, the most rigorous method of software development available today is the use of Formal Methods. Possibly the most famous example of their successful use is the driverless line 14 of the Paris metro.
Formal specification gives us the power to clearly express our meaning, across natural language barriers. Just as legal language was developed to prevent misinterpretation of law, formal specification was developed to prevent misinterpretation of specifications. This unambiguity means that formal specifications can easily be automatically processed by software, unlike natural language. Formal specifications can be automatically checked for ambiguity, incompleteness, and contradiction. They can also be refined in stages from abstract to concrete specifications.
While programming languages are formal enough to be automatically processed, they force the author to think about how functionality can be produced. Formal specifications allow the author to specify what the desired behaviour is first, before considering implementation. Many software faults arise at the design stage because of conflicting or misunderstood requirements. The use of formal methods can highlight these mistakes at a stage where they are more easily spotted and rectified. Once the specification is correct and complete, the final product can be produced in automatic and semi-automatic stages. Formal methods are less widely used than their proponents would like. The specifications can seem cryptic to the uninitiated, and the mathematics involved puts many people off. There is a perception that formal methods do not involve the same creativity as programming. But as Mr. Andrew Harry says:
There are as many ways of writing a formal specification as there are of programming it. Needless to say, only a few of these ways are good.
Despite their "public relations" diffculties, formal methods are indispensible in the development of safety critical systems, where correctness is of the utmost priority.
The authors have not found any EVS developed using formal methods.