Accession Number : ADA324036

Title :   STeP: The Stanford Temporal Prover,

Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Manna, Zohar ; Anuchitanukul, Anuchit ; Bjorner, Nikolaj ; Browne, Anca ; Chang, Edward

PDF Url : ADA324036

Report Date : JUN 1994

Pagination or Media Count : 47

Abstract : We describe the Stanford Temporal Prover (STeP), a system being developed to support the computer-aided formal verification of concurrent and reactive systems based on temporal specifications. Unlike systems based on model-checking, STeP is not restricted to finite-state systems. It combines model checking and deductive methods to allow the verification of a broad class of systems, including programs with infinite data domains, N-process programs, and N-component circuit designs, for arbitrary N. In short, STeP has been designed with the objective of combining the expressiveness of deductive methods with the simplicity of model checking. The verification process is for the most part automatic. User interaction occurs mostly at the highest, most intuitive level, primarily through a graphical proof language of verification diagrams. Efficient simplification methods, decision procedures, and invariant generation techniques are then invoked automatically to prove resulting first-order verification conditions with minimal assistance. We describe the performance of the system when applied to several examples, including the N-process dining philosopher's program, Szymanski's N-process mutual exclusion algorithm, and a distributed N-way arbiter circuit.

Descriptors :   *CONCURRENT ENGINEERING, *SYSTEMS ANALYSIS, *COMPUTER PROGRAM VERIFICATION, ALGORITHMS, DATA MANAGEMENT, COMPUTER AIDED DESIGN, DISTRIBUTED DATA PROCESSING, COMPUTER COMMUNICATIONS, REAL TIME, COMPUTER LOGIC, CIRCUIT ANALYSIS, DEBUGGING(COMPUTERS), EXECUTIVE ROUTINES.

Subject Categories : Computer Systems

Distribution Statement : APPROVED FOR PUBLIC RELEASE