A panacea or academic poppycock: formal methods revisited

摘要

Many formal methods have been proposed to improve software quality. These include new specification and modeling languages as well as formal verification techniques, such as model checking and theorem proving. This paper describes several ways in which tools supporting formal methods can help 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 practical software development. To overcome this problem, this paper describes a number of needed improvements - in techniques for requirements capture, in languages, in specifications and models, in code quality, and in code verification techniques - which could lead to more widespread use of formal methods and their support tools in practical software development.