The role of formal methods in developing safety-critical software

Formal methods use the rigour of mathematics to strengthen the process of software development, leading to lower risk, higher quality and better control of costs and timescales. The use of these methods is growing and practical experience is already quite widespread. Nevertheless, several fallacies still surround formal methods-for example that they are primarily for proving that programs are correct, that they involve complex mathematics, that they increase the cost of development, and that they are incomprehensible to clients. Belief in these fallacies inhibits more widespread use of formal methods by engineers, which damages companies commercially and probably reduces system safety. The article describes the characteristics of the methods, refutes some fallacies, and describes projects in vehicle and traffic control