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