Formal Specification and Run-time Monitoring within the Ballistic Missile Defense Project
Loading...
Authors
Caffall, Dale S.
Cook, Thomas
Drusinsky, Doron
Michael, James Bret
Shing, Man-Tak
Sklavounos, Nicholas
Subjects
Advisors
Date of Issue
2005
Date
Publisher
Language
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 runtime recovery from formal requirement violations.
Type
Technical Report
Description
Series/Report No
Department
Identifiers
NPS Report Number
NPS-CS-05-007