Evaluation of Program Specification and Verification Tools for High Assurance Development
dc.contributor | Naval Postgraduate School (U.S.) | |
dc.contributor.author | Ubhayakar, Sonali | |
dc.contributor.author | Bibighaus, David | |
dc.contributor.author | Dinolt, George | |
dc.contributor.author | Levin. Timothy E. | |
dc.date.accessioned | 2012-07-11T15:49:28Z | |
dc.date.available | 2012-07-11T15:49:28Z | |
dc.date.issued | 2003-09-00 | |
dc.identifier.citation | Proceedings of the International Workshop on Requirements for High Assurance Systems, Monterey, CA, September 2003, pp. 43-47. | |
dc.identifier.uri | http://hdl.handle.net/10945/7117 | |
dc.description.abstract | 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. | en_US |
dc.publisher | Naval Postgraduate School (U.S.) | en_US |
dc.rights | This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States. | en_US |
dc.title | Evaluation of Program Specification and Verification Tools for High Assurance Development | en_US |
dc.type | Article | en_US |
dc.subject.author | Formal specification | en_US |
dc.subject.author | formal methods | en_US |
dc.subject.author | high assurance | en_US |
dc.description.distributionstatement | Approved for public release; distribution is unlimited. |