Accession Number : ADA329515

Title :   SDVS 13 Tutorial

Corporate Author : AEROSPACE CORP EL SEGUNDO CA

Personal Author(s) : Menas, T. K. ; Filippenko, I. V.

PDF Url : ADA329515

Report Date : 30 SEP 1994

Pagination or Media Count : 230

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, firm ware, 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 13 Users' Manual 1 should be consulted for a more comprehensive account.) The tutorial description is embedded in numerous examples of proofs in SDVS.

Descriptors :   *COMPUTER PROGRAMS, *COMPUTER PROGRAM VERIFICATION, *MACHINE TRANSLATION, COMPUTER PROGRAM DOCUMENTATION, ALGORITHMS, SOFTWARE ENGINEERING, USER MANUALS, COMPUTER LOGIC, COMPUTER ARCHITECTURE, COMPUTER APPLICATIONS, ADA PROGRAMMING LANGUAGE, DEBUGGING(COMPUTERS), COMPUTER PROGRAM RELIABILITY, FIRMWARE.

Subject Categories : Computer Programming and Software
      Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE