@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Name: SDVS (State Delta Verification System)
Keywords: state deltas/temporal logic, symbolic execution, simplifiers,
partial and complete decision procedures, translators.
Description:
Semantics: operational semantics; logic equivalent (in expressibility
strength) to "until" (the strongest of the classical temporal
operators)
Deductive machinery: dynamic aspect of proof (symbolic execution,
induction, cases); static aspect of proof (complete and partial
decision procedures/solvers, axioms, rewrite rules)
Dynamics: proof developed interactively and then later executed in
batch mode; an interactive
session typically involves the invocation of various query
commands to determine the current state of the proof,
the simplification of expressions, ``popping back'' to
previous states in the proof and trying a different
strategy, etc.;
hierarchical proof development via lemmas (static and dynamic).
Persistence: theorems/lemmas/formulas and proofs can be saved and restored;
facilities for naming objects, replaying proofs, and generating
proof transcripts.
The State Delta Verification System (SDVS), under development and use
at The Aerospace Corporation for over a dozen years, is a system for
writing and checking proofs about the course of a computation, usually
called ``correctness'' proofs. SDVS can be used to check microcode
implementation correctness proofs, program verification proofs (e.g.
liveness and safety for Ada programs), or hardware correctness proofs
(e.g. liveness and safety for VHDL hardware descriptions).
As a test of the system's microcode correctness capabilities, SDVS was
used to analyze most of the instruction set of the BBN C/30 computer.
A major Ada verification effort involved command code from the
Midcourse Space Experiment (MSX), and the VHDL capability is
demonstrated by the TAXIchip project.
The user communicates to SDVS through several languages. The proof
language is used to write the proof that the system will check. The
state delta language is used to write the theorems to be proved and to
describe the relevant programs and specifications. The user-interface
language allows for interactive proof building, querying, and so on.
Finally, there is a module that translates from a subset of ISPS, from
a subset of Ada, and from a subset of the hardware description
language VHDL into state deltas.
Technically, SDVS aids in the writing and checking of proofs of state
deltas. For example, state deltas can specify claims of the form ``If
P is true now, then Q will become true in the future.'' If P is (the
translation of) a program (perhaps with some initial conditions) and Q
is an output condition, then the above claim is an input-output
assertion about P. SDVS can also specify (and prove) claims of the
form ``If P is true now, then Q is true now.'' In this case, if P is
a (state delta representing a) program or hardware description and Q
is a (state delta representing a) specification, then the above claim
asserts the implementation correctness of P with respect to Q.
SDVS can also prove claims of the form ``If P is true now, then Q will
always be true in the future,'' or until some other condition becomes
true. Finally, SDVS can be used to specify state-transition
invariants.
The ``if-now, then-later'' statement above is the basic building block
of state deltas. It can be thought of as a specification of a state
change, with P being the ``precondition'' (the condition allowing the
state change to occur) and Q the ``postcondition'' (the description of
the state after the change has occurred). The connection with
standard temporal logic is given in the last reference of the
documentation section below.
The proof language can be divided into two parts, the dynamic and the
static. The dynamic part controls the state transitions made by the
system. There are constructs for proof by symbolic execution for
straight-line code, proof by cases for branching code, and proof by
induction for loops. In addition, there are several more-specialized
proof commands, such as the command to sequentialize two
simultaneously true state deltas. Of course, when a symbolic
execution command has caused the system to arrive at a new state, a
static proof may be needed to verify that new relations do in fact
hold, i.e., they follow from the facts known explicitly about the new
state (in order to show that the postcondition is true and the goal is
reached, or to show that a precondition is true and a new state delta
may be applied.)
The static part of the proof language deals with proving that certain
assumptions imply certain conclusions about a given state. For simple
domains where efficient decision procedures exist and are implemented,
the system will be able to derive all conclusions without any
user-input proof. Examples are equality over uninterpreted function
symbols, a fragment of naive set theory, and linear arithmetic. For
more complicated domains, the user writes. proofs by having the system
notice incrementally more difficult conclusions, where the newly
verified conclusions are stored and used as facts on which to base the
next conclusion. The derivation from a given set of facts to the next
conclusion may be automatic in some cases, or it may require the user
to designate that an axiom or a previously proved lemma is to be
applied. We incorporate the Nelson-Oppen simplifier and cooperating
decision procedure paradigm, "partial decision procedures" for
nondecidable or nonefficiently decidable theories of bitstrings and
arithmetic, among others. We also use EKL as a backup module to
bolster our own quantification handling capabilities.
SDVS may be run in interactive mode, batch mode, or, as in most real
applications, as a combination of the two. In interactive mode the
user writes the proof in SDVS with help from system prompts, with the
system executing each proof command as it is written. Expressions are
written in standard infix notation (e.g. x+y). In batch mode the
proof is written either by the SDVS dump-proof command and write
command, or in an editor, and then is executed in SDVS with no further
user interaction. Most commonly, a partial proof is written
interactively, stored, and then rerun in batch mode at a later time
when the proof-writing process is being continued.
Contact persons:
Leo Marcus
The Aerospace Corporation
P.O. Box 92957, mail station M1-055
Los Angeles, CA 90009
(310)336-4541
marcus@aero.org
Ranwa Haddad
The Aerospace Corporation
P.O. Box 92957, mail station M1-055
Los Angeles, CA 90009
(310)336-5288
haddad@aero.org
User group support: reports distributions list
Currently our academic users are at Cambridge University, George Mason
University, Johns Hopkins University, and University of California at
Santa Barbara. Other users are at National Security Agency, Naval
Research Laboratory, Rome Laboratory, Motorola, ORA, Trusted
Information Systems, and MITRE Corp.
Pragmatics: Strengths include practical proof system, capability to
deal with real/standard computer languages, and demonstrated applicability
(microcode, software, and hardware).
Weaknesses: initial hurdle of learning the "unorthodox" state
delta language, non-scalability of certain kinds of proofs.
Documentation:
J. V. Cook, ``Verification of the C/30 Microcode Using the State
Delta Verification System (SDVS),'' in Proceedings of the 13th
National Computer Security Conference (Washington, D. C.), pp. 20-31,
National Institute of Standards and Technology/National Computer Security
Center, Oct. 1990.
J. V. Cook, I. V. Filippenko, B. H. Levy, L. G. Marcus, and T. K. Menas,
``Formal Computer Verification in the State Delta Verification
System (SDVS),'' in Proceedings of the AIAA Computing in Aerospace
Conference (Baltimore, MD), American Institute of Aeronautics and
Astronautics, Oct. 1991.
M. M. Cutler, ``Verifying implementation correctness using the State Delta
Verification System (SDVS),'' in Proceedings of the 11th National
Computer Security Conference, National Bureau of Standards/National Computer
Security Center, Oct. 1988.
I. V. Filippenko, ``VHDL Verification in the State Delta Verification
System (SDVS),'' in Proceedings of the 1991 International Workshop
on Formal Methods in VLSI Design, (Miami, Fla), ACM, Jan. 1991.
B. H. Levy, ``An Overview of Hardware Verification Using the State
Delta Verification System (SDVS),'' in Proceedings of the 1991
International Workshop on Formal Methods in VLSI Design (Miami, Fla), ACM,
Jan. 1991.
T. K. Menas, J. M. Bouler, J. E. Doner, I. F. Filippenko, B. H. Levy, and L.
Marcus, ``Overview of the MSX Ada Verification Experiment using SDVS,'' Tech.
Rep. ATR-93(3778)-6, The Aerospace Corporation, Sept. 1993.
T. K. Menas. "The Relation of the Temporal Logic of the State Delta
Verification System (SDVS) to Classical First-Order Temporal
Logic," Tech. Rep. ATR-90(5778)-10, The Aerospace Corporation,
Sept. 1990.
Resource requirements:
SDVS 13 currently runs under Franz Allegro Common Lisp (FACL) 4.2 on
either Sparc 2 or Sparc 10 processors. Aerospace has a ``runtime
generator'' license agreement from Franz, Inc., which allows Aerospace
to deliver SDVS to end users without requiring them to purchase a
Common Lisp system (the runtime version removes some features from the
development version of Common Lisp).
SDVS assumes that the underlying operating system is
Unix, Sun OS 4.1, or equivalent.
Where-to-get-it:
To request an SDVS software request form, write to sdvs-requests@aero.org.
info source/date] Leo Marcus July95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%