Accession Number:

ADA370002

Title:

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

Descriptive Note:

Final rept. 1 Jun 95-31 Mar 99

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1999-06-30

Pagination or Media Count:

30.0

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE