Skip to content
Hamilton Archive
0 / 17
Pre-launch Review

The Relationship Between Design and Verification

The Relationship Between Design and Verification

Section titled “The Relationship Between Design and Verification”

Margaret H. Hamilton and Saydean Zeldin, Higher Order Software, Inc., 1979

A system development process is itself a system that develops another system. Requirements are inputs; specifications are outputs. “One engineer’s requirements could be another engineer’s specifications.” The paper opens with this framing, establishing the recursive nature of development that would become central to Hamilton’s later work.

The key insight: “For each step of design, there should be a ‘counterstep’ of verification.” But this does not mean a one-to-one correspondence. Sometimes design IS verification — when design techniques are included specifically to prevent errors, “some types of verification requirement are designed out of the system.” This is the first clear articulation of the idea that would eventually become the preventative paradigm.

Three Phases of Verification

Section titled “Three Phases of Verification”

Hamilton and Zeldin define a hierarchy of verification that eliminates work at each level:

  1. Conceptual phase: Eliminate certain types of verification entirely by following design principles. If a system is designed so that interface errors cannot exist by construction, testing for interface errors is unnecessary.

  2. Static phase: Check correct use of principles automatically and statically. This catches errors from incorrect application of the methodology without running the system.

  3. Dynamic phase: Verify only the performance of particular algorithms — the fraction of the system that cannot be verified by design or static analysis alone.

The Rationale for Methodology

Section titled “The Rationale for Methodology”

A remarkably practical section addresses the challenge of convincing organizations to adopt formal methods. Hamilton’s recommended approach: select a module within the project’s existing environment and show the differences in definition using the new methodology versus existing methods. “The power of new concepts is often realized when those errors are uncovered in an engineer’s own system, especially when that module is thought to be already working!”

On the “smart people don’t need methodology” argument: “An effective methodology, however, applied in common by several smart people, would far exceed the advantages of each smart person applying techniques in an ad hoc manner, since all the intricacies of a complex system are by nature beyond the grasp of any human being.”

On the concern that methodology constrains creativity: “An effective methodology provides more constraints for the designers but only in the area of preventing the production of errors. As a result, creative designers should be less constrained in producing better designs.”

AXES: The Specification Language

Section titled “AXES: The Specification Language”

AXES (the name derives from the axioms) is described as “a formal notation for writing definitions of systems.” It is not a programming language but “a complete and well-defined language capable of being analyzed by a computer.” AXES provides mechanisms for defining data types, functions, and structures.

The three primitive control structures are defined: dependent functions (composition/join), independent functions (parallel/include), and selection of functions (partition/or). Every node in an AXES definition represents a controller relating functions to input and output, integrating four viewpoints: definition, description, implementation, and execution.

A critical formal property: single-reference, single-assignment. Each variable represents an object state, not a memory location. This enables distributed processing because there are no shared mutable state conflicts.

The Reject distinguished value is introduced as a member of every data type. If an input value maps to Reject as output, an error has been detected. Functions applied to inputs containing Reject may either propagate it (error propagation) or recover from it (error handling). This formalization makes error states explicit in the type system.

GCD: A Complete Worked Example

Section titled “GCD: A Complete Worked Example”

The Greatest Common Divisor algorithm is specified in AXES from two perspectives. First, an implicit definition using derived operations with axioms about Factor, Entails, And, Not, and equality. Second, an explicit algorithm using or, coor, join, and coinclude structures.

The explicit algorithm demonstrates that all non-primitive structures can be decomposed into primitives. The coor structure is traced through its definition to show how it reduces to join, or, and each (the primitive form of include).

Two implementation assumptions are highlighted: the expression (x, y) <- (y, x) must be atomic (compiler-dependent), and single-statement restart capability must be available — “This type of ultrareliability is often required, for example, in aerospace real-time applications.”

Section titled “Navpak: A Real-World System”

The satellite navigation system “Navpak” provides the real-world demonstration. Navpak updates navigational parameters of Earth-referenced satellites using imaging data, determining orbit and attitude from landmark observations with varying degrees of automation from manual correlation to fully automatic processing with manual override.

The key design feature: the user has the option to incorporate a measurement immediately at any step, or automatic processing continues. This manual override capability is formally specified within AXES, not bolted on as an afterthought. The system is recursive — it calls itself for each successive landmark.

Experiences with HOS

Section titled “Experiences with HOS”

Five categories of practical application provide what amounts to an honest assessment of HOS in the field:

AGC Operating System Respecification. Respecifying the Apollo Guidance Computer operating system in AXES revealed that “many of the development errors that occurred in the application programs using the OS would not have occurred if the AGC OS had certain other inherent properties; for although the AGC OS had properties of hidden data, it did not have properties of hidden timing.” Encapsulating state without encapsulating timing was insufficient.

PLRS (Position Locator Reporting System). The most complex module of an ongoing project was specified in AXES, revealing 16 categories of questionable areas. The demonstration was immediate and concrete: problems in a system the developers believed was already working.

Universal Flowcharter. Designed in AXES, implemented in Pascal. “Any errors that occurred in implementation were in those areas where the specification was not complete before implementation.” Modules with complete specifications had almost no implementation errors; incomplete ones were error-prone and took longer to debug.

Common observations across projects: The process of defining AXES modules always produces identification of commonality between modules. Interface errors are always found in existing systems. The control map technique serves as an accelerated learning tool for new project members.

References

Section titled “References”

The paper contains extensive references to HOS internal publications, Hamilton and Zeldin’s earlier work, and related formal methods literature.

Section titled “Related Documents”