Evaluation of Program Specification and Verification Tools for High Assurance Development
Sonali Ubhayaker, David Biblighaus, George W. Dinolt, Tim Levin · 2003
A key decision in the development of high assurance software is that of choosing a formal methods tool. This paper describes a methodology to select a formal methods tool for use in the development of high assurance software. Some of the factors that make a tool suitable to the task can be evaluated with a desk check, while others can only be appreciated by "hands on" testing. We describe the application of our methodology to a broad set of currently available formal methods tools, including a hands-on evaluation of one of the tools. The impact of the tools on the project development is also discussed.