A Formal Methods Workbench for Critical Systems

Abstract

The research performed in this project enhanced the PVS formal verification system to provide improved support for the development and assurance of fault-tolerant and safety-critical systems. The capabilities developed are freely available in the publicly distributed version of PVS. In addition, new and more systematic methods were developed for verifying certain kinds of critical systems (including self-stabilizing ones), and an exciting new application of formal methods to the problems of automation surprises and mode confusions in advanced cockpits was pioneered. Finally, new fault-tolerant algorithms and architectures were developed, and some significant demonstration applications of formal methods were performed.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 22, 2000
Accession Number
ADA378690

Entities

People

  • John Rushby

Organizations

  • SRI International

Tags

Communities of Interest

  • Biomedical
  • C4I
  • Energy and Power Technologies
  • Engineered Resilient Systems
  • Ground and Sea Platforms
  • Human Systems
  • Space

DTIC Thesaurus Topics

  • Aircrafts
  • Algorithms
  • Artificial Intelligence
  • Coding
  • Computational Fluid Dynamics
  • Computer Programming
  • Computer Science
  • Computers
  • Control Systems
  • Debugging
  • Embedded Systems
  • Instruction Set Architecture
  • Operating Systems
  • Reliability
  • Software Development
  • Theoretical Computer Science
  • Two Dimensional

Readers

  • Software Engineering.
  • Systems Analysis and Design