A Scalable, Reconfigurable, and Dependable Time-Triggered Architecture

Abstract

The research performed in this project began with a study and comparison of time-triggered bus architectures for critical systems and with development of flexible methods for scheduling time-triggered systems. Later work focused on automated synthesis and refutation (debugging) and developed a new method for bounded model checking over infinite domains based on integration of efficient decision procedures with SAT solving. The method was then extended to automated verification. Implementations of the method are available from SRI in our tools ICS and SAL. The approach pioneered in this project for combining decision procedures with a SAT solver has now become the dominant one for bounded model checking and automated verification.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 2003
Accession Number
ADA431078

Entities

People

  • John M. 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

  • Air Force
  • Air Force Research Laboratories
  • Aircrafts
  • Algorithms
  • Application Software
  • Computer Programming
  • Computer Science
  • Computers
  • Control Surfaces
  • Control Systems
  • Debugging
  • Failure Mode And Effect Analysis
  • Information Systems
  • Operating Systems
  • Systems Engineering
  • Transport Aircraft
  • United States

Fields of Study

  • Computer science

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Mathematical Modeling and Probability Theory.
  • Software Engineering.