Evaluation of Program Specification and Verification Tools for High Assurance Development
Levin. Timothy E.
MetadataShow full item record
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.
Showing items related by title, author, creator and subject.
Kremer, Brent. (Monterey, California. Naval Postgraduate School, 1996-06);This thesis analyzes and documents the Army's training development process as it relates to the materiel development of corresponding Army acquisition programs. Training development is a vital necessity for the successful ...
MIT/DRAPER Technology Development Partnership Project : Design, assembly, and test of the launch and flight support and deploymnet system for a gun launched reconnaissance vehicle Shook, Garrett W. (Monterey, California. Naval Postgraduate School, 1998-06-01);The MIT/Draper Technology Development Partnership Project is a two year design and development project between Draper Laboratory and the MIT department of Aeronautics and Astronautics. Overall aims of the project include ...
Boger, Dan C.; Malcolm, David S. (Monterey, California. Naval Postgraduate School, 1993-02); NPS-AS-93-012There are two different approaches, the disjoint and sequential models, which attempt to account for differences between development unit cost and production unit cost. The disjoint model uses a production cost improvement ...