Formal Specification and Run-time Monitoring Within the Ballistic Missile Defense Project

Abstract

This report describes the application of formal specifications and run-time monitoring within the U.S. Ballistic Missile Defense Advanced Battle Manager (ABM) project in an effort that is amongst the most comprehensive application of formal methods to a large-scale safety-critical software application ever reported. This project is unique in the following aspects: (i) formal specification assertions are being developed during the UML modeling phase, that is, before code development, (ii) all specification requirements are simulated under a variety of input and timing scenarios before being deployed, (iii) requirements are written in metric temporal logic with time-series constraints, (iv) run-time monitoring is used as the primary verification technique, and (v) temporal assertions are used for run-time recovery from formal requirement violations.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 2005
Accession Number
ADA436597

Entities

People

  • Dale S. Caffall
  • Doron Drusinsky
  • James Bret Michael
  • Mantak Shing
  • Nicholas Sklavounos
  • Thomas Cook

Organizations

  • Naval Postgraduate School

Tags

Communities of Interest

  • Biomedical
  • C4I
  • Materials and Manufacturing Processes
  • Space

DTIC Thesaurus Topics

  • Acquisition
  • Application Software
  • Command And Control
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Debugging
  • Defense Systems
  • Engineering
  • Jet Propulsion
  • Software Design
  • Software Development
  • Specifications
  • System Of Systems
  • Systems Engineering
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Missile Defense Systems.
  • Software Engineering.