@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%