Bibliographic sketch
Summary
The technical theme behind HARQ05 is that behavioural assumptions must be treated as first-class artefacts. In concurrent and component-based settings, correctness depends not only on what a component computes, but on how it interacts: which messages can be exchanged, what ordering is expected, which failures are possible, and what the environment is assumed to provide.
The paper’s viewpoint can be described as a bridge between two perspectives. The first is semantic: define a small model that explains the meaning of a component’s behaviour. The second is compositional: define how components connect, then ask what properties survive composition. By making interaction explicit, the method turns “integration surprises” into checkable mismatches.
A practical takeaway is methodological: choose a minimal model that answers your question and then choose a check that is feasible. Sometimes that check is a lightweight exploration (a model-checking run on an abstract model); sometimes it is a proof about a critical part of a protocol; sometimes it is an invariant enforced by tests and runtime checks. The selection is driven by constraints, not by ideology.
Key ideas
- Interaction is part of the specificationInterfaces should describe allowed sequences of actions, not only data shapes.
- Composition changes meaningA component’s guarantees depend on assumptions; composition can violate assumptions silently.
- Minimal models enable feasible checksAbstraction is a tool for making analysis repeatable and explainable.
Diagram
Related pages
- Behavioural contractsAssume/guarantee reasoning and composition.
- Model checking primerA practical view of state exploration and abstraction.
- Projects hubProject-style topic pages that apply similar ideas.