Evaluation of Program Specification and Verification Tools for High Assurance Development

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2003
Accession Number
ADA435402

Entities

People

  • David Biblighaus
  • George Dinolt
  • Sonali Ubhayaker
  • Tim Levin

Organizations

  • Naval Postgraduate School

Tags

Communities of Interest

  • Energy and Power Technologies
  • Human Systems
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Computer Programming
  • Concrete
  • Consistency
  • Construction
  • Discriminators
  • Language
  • Lisp Programming Language
  • Operating Systems
  • Programming Languages
  • Security
  • Software Design
  • Software Development
  • Specifications
  • Spiral Development
  • Standards
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Instructional Design and Training Evaluation.
  • Software Engineering.