STeP: A Tool for the Development of Provably Correct Reactive and Real-Time Systems

Abstract

This research is directed towards the implementation of a comprehensive toolkit for the development and verification of high assurance reactive systems, especially concurrent, real time, and hybrid systems. For this, we have designed and implemented the STeP (Stanford Temporal Prover) verification system. STeP is a tool for the computer aided formal verification of reactive systems, including real time and hybrid systems based on their temporal specification. STeP integrates model checking and deductive methods to allow the verification of a broad class of systems, including parameterized (N component) circuit designs, parameterized (N process) programs. and programs with infinite data domains.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 30, 1999
Accession Number
ADA370002

Entities

People

  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Automata
  • Case Studies
  • Complex Systems
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Graphical User Interface
  • Hybrid Systems
  • Language
  • Set Theory
  • Standards
  • Students
  • Systems Engineering
  • Theoretical Computer Science

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Software Engineering