Developing safety-critical systems: the role of formal methods and tools

In recent years, many formal methods have been proposed to improve the quality of safety-critical software systems. These methods include new specification and modeling languages as well as formal verification techniques, such as model checking and theorem proving. This paper describes numerous ways in which tools supporting formal methods can improve the quality of both software code as well as software specifications and models. However, while promising, formal methods and their support tools are rarely used in software practice. To overcome this problem, I propose several needed improvements, which could lead to more widespread use of formal methods in the development of safety-critical systems and software.