Accession Number : ADA291143

Title :   SDVS 11 Tutorial,

Corporate Author : AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP

Personal Author(s) : Menas, T. K.

PDF Url : ADA291143

Report Date : 30 SEP 1993

Pagination or Media Count : 232

Abstract : This report is a tutorial for the State Delta Verification System (SDVS), an automated system developed at The Aerospace Corporation for use in formal computer verification. SDVS helps users write and check mathematical proofs of computer correctness at the hardware, firmware, and software levels. Currently, SDVS is capable of verifying properties of computer descriptions or programs written in three computer languages. These languages are subsets of the hardware description languages VHDL and ISPS, and of the Ada programming language. In addition, SDVS may be used to verify the validity of a large class of formulas of first-order temporal logic. This tutorial contains a description of most, but not all, of the proof capabilities of SDVS. (The SDVS 11 Users' Manual 1 should be consulted for a more comprehensive account.) The tutorial description is embedded in numerous examples of proofs in SDVS. (AN)

Descriptors :   *SOFTWARE ENGINEERING, *COMPUTER PROGRAM VERIFICATION, COMPUTER PROGRAM DOCUMENTATION, DATA PROCESSING, COMPUTATIONS, AUTOMATION, COMPUTER LOGIC, PROGRAMMING LANGUAGES, SEMANTICS, MATHEMATICAL LOGIC, COMPUTER ARCHITECTURE, SYSTEMS ANALYSIS, DYNAMIC PROGRAMMING, ADA PROGRAMMING LANGUAGE, SYNTAX, EXECUTIVE ROUTINES.

Subject Categories : Computer Programming and Software
      Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE