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.
Martinez, T.; Agrawal, B.N. (2008);This paper discusses two optical beam control testbeds developed at the Spacecraft Research and Design Center, Naval Postgraduate School, to evaluate and develop control techniques for jitter and adaptive optics control. ...
Corley, M.S.; Santiago, F.; T. Martinez; Agrawal, B.N. (2011);The Navy is interested in horizontal laser propagation studies in a maritime environment, near the ocean surface, for applications including imaging and high-energy laser propagation. The Naval Postgraduate School (NPS) ...
Cao, Lan; Ramesh, Balasubramaniam; Abdel-Hamid, Tarek (2010-12);Changes in the business environment such as turbulent market forces, rapidly evolving system requirements, and advances in technology demand agility in the development of software systems. Though agile approaches have ...