@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

Name:  EHDM (Enhanced Hierarchical Development Methodology)

Keywords:  Specification/Verification Environment, Hierarchical
  Development Methodology, Parameterized Modules, Higher-order Logic,
  subtyping, Arithmetic Decision Procedures, Hoare Logic, Multi-Level
  Security

Description: 
  Semantics: Classical Higher-Order Logic with predicate subtypes;
    Hoare Logic.  Axioms may be introduced freely; definitions (which
    may be recursive) provide conservative extension; hierarchical
    specifications related by theory interpretation.

  Deductive machinery: Typechecking resolves name references and
    ensures type-consistency of the specification; typechecking can
    generate proof obligations; For proof checking, user supplies
    relevant lemmas and definitions as premises for the
    theorem.  The resulting implication is Skolemized for manual and
    heuristic  instantiation.  Powerful ground decision procedures  are
    then applied for propositional logic and linear arithmetic 
    equalities/inequalities.   The IPC is an Emacs-based tool for
    incremental, interactive proof development.   Hoare Sentence Prover
    is used for checking proofs of imperative programs (which can be
    automatically translated to Ada).  Mappings specified between
    specifications generate proof obligations required for theory
    interpretation; same mechanism allows demonstration of
    consistency of axiomatically-specified theories.  Flow-analyzer
    for multilevel security analysis.
  Dynamics:  Theories along with proofs are developed and saved as
    parameterized modules.   
  Persistence:  The current context consisting of the current modules
    along with their status (parsed, typechecked, proved, etc.) is
    saved so that a new session can be resumed from the current state.

Contact persons: John Rushby, Sam Owre

    Computer Science Laboratory
    SRI International
    333 Ravenswood Avenue
    Menlo Park, CA 94025 USA

    Email {rushby,owre}@csl.sri.com,
    Tel: (415)859-5456/5114
    FAX: (415)859-2844

User group: Used for formal specification and verification of fault
  tolerant algorithms and architectures by SRI and NASA.  In use at
  several other aerospace research centers and also in laboratories
  engaged in secure systems development.
 
Pragmatics:
  Strengths:  Rich type system with predicate subtypes, parameterized
    modules, Refinement hierarchy, Facility for Ada code generation,
    Higher-order logic, Powerful arithmetic decision procedures.
    Proof descriptions allow informal proof to be extracted.
    Has been used (by people other than its developers) to perform
    very hard formal specifications and verifications (e.g., Byzantine
    fault tolerant algorithms, including clock-synchronization) 

  Weaknesses:  Restricted availability.
    Only limited support for interactive proof development and rewriting.
    Proof checking tools are not customizable via tactics.

Documentation: full language and system manuals and tutorial are
   available; several large specifications and verifications are fully
   documented; some smaller examples are being developed.

Applications:
   1. Verification of Lamport and Melliar-Smith's Interactive
      Convergence Algorithm for Byzantine fault-tolerant clock
      synchronization.  EHDM proof identified several flaws in the
      original argument.
   2. Verification of a Schematic Protocol for Byzantine fault-tolerant
      clock synchronization due to Schneider.  Paul Miner at NASA has
      modified this proof and verified the correctness requirements for
      Lundelius and Lynch's fault-tolerant midpoint algorithm.
   3. Verification of a refinement hierarchy for a Reliable Computing
      Platform for digital flight-control applications.  Proof includes
      fault-masking and transient recovery in the presence of skews
      between local clocks.
   4. Formal specification and verification of the "unwinding
      theorems" of classical and intransitive noninterference (a
      formulation of computer security)
   5. Several smaller examples: mini-Cayuga pipelined
      microprocessor, finite Ramsey theorem,
      Oral Messages algorithm for Interactive Consistency and
      Byzantine Agreement. 

Extensions/enhancements: Expect to augment theorem prover with
  technology developed for PVS

Resource requirements:
  implementation language: Common Lisp/CLOS; runs on Sun 3 and Sun 4
    workstations; requires Lucid Lisp licence

  environment support required: uses customized Gnu Emacs as its
    interface; pop-up menus available under SunView;
    typeset specifications require LaTeX; needs 32Mbytes of real
    memory, 50+ Mbytes of swap space, 50 MBytes of disk space.

Where-to-get-it: 
  Distribution controlled by National Security Agency: permission
    granted routinely for US Government agencies, US Companies and
    Universities; no overseas distribution.

  Contact John Rushby at address above for information on procedure
     for requesting permission to use system from NSA.   System
     supplied free of charge (object-code only) on Sun cartridge.
  No ftp distribution.

Info source/date: John Rushby, Aug 5, 1992

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%