Ninth IEEE International Symposium on High-Assurance Systems Engineering (HASE'05)
A Panacea or Academic Poppycock: Formal Methods Revisited
Heidelberg, Germany
October 12-October 14
ISBN: 0-7695-2377-3
Many formal methods have been proposed in recent years 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.