Specification and Validation of Space System Behaviors

Abstract

The NASA Independent Verification and Validation (IV&V) Facility is using formal specification techniques for the IV&V of the flight software for several upcoming missions. Such formal specifications are typically created on the basis of natural-language (NL) requirement specifications that are formalized at a later stage. This paper describes a technique for the discovery of NL requirements by systematic analysis of UML Activity Diagrams and Sequence Diagrams that represent critical mission operational scenarios and sequences. Our technique demonstrates a pattern oriented approach where patterns of NL requirements are mined out of the UML models based on predetermined categories of assertions, including Bounded Eventualities, Loops, Reentrance, and Order and Precedence.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 02, 2010
Accession Number
ADA516732

Entities

People

  • Doron Drusinsky
  • Steven Raque

Organizations

  • Naval Postgraduate School

Tags

Communities of Interest

  • C4I
  • Materials and Manufacturing Processes
  • Space

DTIC Thesaurus Topics

  • Buildings And Structures
  • Case Studies
  • Computers
  • Earth Orbits
  • Filters
  • Kalman Filters
  • Language
  • Natural Languages
  • Orbits
  • Sequences
  • Space Systems
  • Spacecraft
  • Specifications
  • Standards
  • Trajectories
  • Validation
  • Verification

Fields of Study

  • Computer science
  • Physics

Readers

  • Computational Linguistics
  • Computational Modeling and Simulation
  • Cybersecurity.

Technology Areas

  • Space
  • Space - Spacecraft Maneuvers