Formal Verification of Properties of Digital Systems Using an Automated Reasoning System

摘要

This paper describes a part of an ongoing research project whose goal is to develop a formal design verification system based on the use of ITP, an LMA (Logic Machine Architecture) based Interactive Theorem Prover developed at Argonne National Laboratory. Specifically, a Petri net representation for systems is described together with the ITP implementation of a rule-based system for the manipulation of system descriptions. To illustrate the representation and the capabilities of the system under development, the Draper Laboratories Fault-Tolerant Processor is used as an example. Results concerning the formal verification of the fault-tolerant properties of this system are described. 17 refs., 7 figs. (ERA citation 11:033465)