When developing or modifying software, engineers can use formal methods – a range of mathematical techniques for modelling the software and testing how it will work – to detect and prevent errors at every stage of the process. These methods of validation (checking that the software specification meets the user requirements) and verification (ensuring that the software works correctly, satisfying the specification) are crucial in contexts such as transport or aerospace, where failure could have catastrophic results.
Existing formal methods provide rich mathematical languages for modelling and reasoning about correct system behaviour. However, it is difficult to scale them for complex systems in which a software-based controller manages many features or controls a large proportion of a system’s functions – for example, a control system that supervises a large volume of traffic on a rail network.
Another issue with formal methods approaches is slow uptake in industry, where the potential improvements in reliability, and savings in testing and reworking costs, are not always recognised and the techniques are perceived as being inaccessible to non-academic engineers.