The deductive theory manager: a knowledge based system for formalverification

摘要

Formal verification tools and techniques are difficult andexpensive to apply. To make verification of large, complex systems morepractical, TRW is developing the deductive theory manager (DTM). Aknowledge-based tool that integrates with the Gypsy verificationenvironment (GVE), the DTM supports the construction of deductivetheories and applies them to proofs. Knowledge bases applicable to avariety of projects, and one specific to the army secure operatingsystem (ASOS) proofs, are simultaneously under development. The authorsdescribe the underlying philosophy of the verification strategy on whichthe DTM is based, present the DTM architecture, and illustrate DTMknowledge engineering and proof processing with a case study