Skip to content
Chapter 2 — Modeling  ::  §2.3

§2.3 Behavioral Models: What May Happen?

A structural model holds a system still; a behavioral model lets it move. It suppresses most of what a component is and keeps what it may do over time — the states a job may occupy, the transitions permitted between them, and the orderings those transitions allow or forbid. Where a dependency graph answers what is connected to what?, a behavioral model answers a question that only arises once time is admitted: what may happen, and in what order?

2.3.1 The Canonical Move: States, Transitions, and Executions

Engineering has represented behavior this way for a long time. A finite-state machine names the legal states of a system and the transitions between them; a labeled transition system adds the events that label those transitions; statecharts add hierarchy and concurrency so that large behaviors stay legible;11. David Harel, “Statecharts: A Visual Formalism for Complex Systems,” Science of Computer Programming 8, no. 3 (1987): 231–74, https://doi.org/10.1016/0167-6423(87)90035-9. a temporal specification describes a property of whole executions rather than of any single state. These forms differ in expressiveness, but they share one reduction: they keep the states and the transitions, and they discard the code that implements each one.

That reduction is what makes behavior checkable. A job-processing service described only through its handlers, database writes, and retries hides the very question an engineer most needs to ask — can the system reach a state it should never occupy? The same service, reduced to a handful of states and the transitions between them, turns that question into one a person or a tool can actually answer (Figure 2.3-1).

Canonical behavioral model: reduce an implementation to states and transitions A behavioral opener. A neutral implementation slab reduces to a state model: IDLE starts RUNNING, which finishes to DONE or fails to FAILED. A struck-through dashed arc marks the forbidden direct IDLE-to-DONE transition (no skipping RUNNING). Caption: Question, Semantics, Typical analysis. Blue ground marks the behavioral family. Behavioral model — what may happen, in what order? IMPLEMENTATION handlers · retries writes · logging … reduce to IDLE RUNNING DONE FAILED start finish fail no such transition (no skipping) Question: What may happen, and in what order? Semantics: node = a legal state; edge = a permitted transition; a path = an admitted execution. Typical analysis: reachability, safety, liveness.
Figure 2.3-1. The behavioral move: states and transitions. A model keeps the legal states and the permitted transitions and discards the code; the transition it omits — here the skip from IDLE straight to DONE — is the behavior it forbids. Its analyses search for a reachable bad state or a required event that never arrives.

A node is a legal state; a directed edge is a permitted transition; a path through the graph is an execution the model admits. The key content is often negative: the transitions the model omits are exactly the behaviors it declares illegal. Once behavior is explicit, the questions form a progression from local to global — is this single transition legal? is this state reachable at all? can a legal execution reach a forbidden state? can the system deadlock? must some event eventually occur? The first are safety questions, which a single bad execution refutes; the last is a liveness question, which no finite good execution can establish, because the failure is the system running forever without the required event. A model can make either expressible, and the choice of check — transition validation, reachability search, invariant checking, or temporal model checking22. Christel Baier and Joost-Pieter Katoen, Principles of Model Checking (MIT Press, 2008). — follows from the shape of the property rather than from a preference for one method.

A behavioral model does not make the system behave. It makes the behavior something one can reason about before it runs.

2.3.2 DocAble: Recovery Ordering

DocAble has one behavioral obligation whose violation is quiet and expensive. When a job falls back to a recovery path, the durable artifact and the database record that points at it must be written in the right order: the record may not name an artifact that has not yet been published. Reduced to its states, that concern is a small model.

MODEL CARD

Recovery-ordering model · Behavioral

  • Engineering question — In what order may recovery publish an artifact and update the record that refers to it?
  • Model — a transition system over the recovery lifecycle; the decisive fact is a transition that does not exist.
  • Property — the database record may refer to the fallback artifact only after that artifact has been durably published.
  • Quality attribute — data integrity; crash-safety.

The recovery lifecycle runs through several states, but the obligation lives in two of them. An artifact is first written locally (FALLBACK_STAGED) and only later published to durable storage (FALLBACK_UPLOADED). The record may advance to DB_UPDATED only from the durable state. Figure 2.3-2 draws the ordering, and the fact that matters is the edge that does not exist: there is no direct FALLBACK_STAGED → DB_UPDATED transition, so the record can never point at a merely-staged, not-yet-durable artifact. Local staging and durable publication are different states, and the whole obligation rides on keeping them apart.

Recovery-ordering model: three legal states and one forbidden edge Three states in legal order. FALLBACK_STAGED transitions on upload success to FALLBACK_UPLOADED, which transitions when durable state is updated to DB_UPDATED. The decisive fact is a forbidden edge: FALLBACK_STAGED may not go directly to DB_UPDATED. Durable state may not name an artifact recovery has not yet published. RECOVERY MODEL FALLBACK_STAGED upload succeeds FALLBACK_UPLOADED durable state updated DB_UPDATED forbidden / absent transition not part of the model The fallback artifact must become durable before database state may refer to it.
Figure 2.3-2. Recovery-ordering model. The decisive fact is the absent transition from FALLBACK_STAGED directly to DB_UPDATED.

Stated over the model, the property is a reachability claim: DB_UPDATED is reachable only through FALLBACK_UPLOADED. That is a property the model exposes and makes checkable — one can search the transition system for any path into DB_UPDATED that skips durable publication. Whether the running recovery path is held to the ordering — whether a transition table refuses the short-circuit step — is a question of enforcement, and it belongs to Chapter 3. The two layers stay separate here: the model exposes the ordering; a mechanism enforces it. This obligation is a hard one — the machinery refuses the violation rather than merely reporting it — but the refusal is Chapter 3's subject, not the model's.

2.3.3 What the Model Makes Checkable

The recovery model answers a safety question — can a bad state be reached? — and one counterexample would settle it. Not every behavioral obligation has that shape. "Every job eventually reaches a terminal state" is a liveness claim: no successful run proves the system can never stall, so the obligation ranges over infinite executions rather than reachable states, and it needs a different checker. Figure 2.3-3 places the three classes side by side.

Behavioral models expose different classes of properties A single behavioral model of states, transitions, and legal sequences forks into three property questions. A local rule asks whether an edge is legal and is answered by a transition check. A reachable-state question asks whether a state can occur and is answered by a state-space search. A temporal property asks whether something will eventually occur and is answered by temporal model checking. All three converge on evidence about behavior. Same model family; different property, different checker. BEHAVIORAL MODEL states · transitions · legal sequences LOCAL RULE REACHABLE-STATE TEMPORAL PROPERTY is this edge legal? can this state occur? will this eventually occur? transition check state-space search temporal model checking EVIDENCE ABOUT BEHAVIOR Same model family; different property, different checker.
Figure 2.3-3. Behavioral models expose different classes of properties. A transition relation can support local legality checks, reasoning over reachable states, or temporal claims over executions. The appropriate checker follows from the property; richer machinery is not automatically stronger for every question.

The point is not that DocAble should apply every one of these techniques. It is that once behavior has an explicit representation, the right form of reasoning becomes available for each kind of property, and the checker follows from the property rather than from habit. The recovery ordering is itself a sharp slice of a larger behavioral model: a DocAble job carries a full lifecycle — queued, leased, remediating, completed or failed — with its own legal transitions. The full lifecycle answers broader workflow questions; the three-state recovery ordering is the sharper reduction for crash-safe publication.

The recovery-ordering model makes an ordering obligation explicit and searchable. It does not, by itself, establish that the implementation realizes the model, prove that this is the right ordering for the product, or decide what should happen when the ordering is violated. It gives engineering a precise object to check and a precise thing to align.

Structural models froze time; this section let it flow but assumed a single actor moving through states. The next question is what happens when several actors reach for the same work at once.

2.3.4 DocAble: Ownership Under Contention

With one worker, who owns this job? has an obvious answer. Add many workers, a crash, and a sweep that reclaims abandoned work, and the same question acquires time and contention: ownership can be claimed, can expire, and can be reclaimed, and a holder that went away can return to find its claim gone. Engineering has a long vocabulary for control over a shared resource: locks and leases,33. Cary G. Gray and David R. Cheriton, “Leases: An Efficient Fault-Tolerant Mechanism for Distributed File Cache Consistency,” in “Proceedings of the Twelfth ACM Symposium on Operating Systems Principles,” special issue, Proceedings of the Twelfth ACM Symposium on Operating Systems Principles (New York), 1989, 202–10, https://doi.org/10.1145/74850.74870. capability and claim relationships, and the lifecycle of a claim from acquisition through expiry to reclamation. An ownership model keeps those relationships and discards the rest — who holds what, on what terms, and for how long.

A claim binds a holder to a resource and carries the facts that make contention decidable: which holder, which generation of claim, and when it expires. The generation is the fact a bare "A owns X" edge cannot express — it distinguishes a current claim from a superseded one. The hard failures do not live in any single transition. They live in the interleavings: the orders in which concurrent claims, expiries, and reclaims can occur. So the characteristic analysis is state-space exploration over those sequences, with an invariant checked at each reachable configuration — the behavioral toolkit of this section pointed at a concurrency question.

DocAble leases each in-flight job to one worker. A lease carries an owner, a monotonically increasing generation, and a lifetime; when a lease looks abandoned it can be reclaimed and the job re-leased to another worker at the next generation.

MODEL CARD

In-flight lease · Ownership

  • Engineering question — Who currently owns this in-flight work, and can a returning stale owner disturb the current claim?
  • Model — a claim relating a worker to a job, stamped with a generation and a lifetime; reclaim advances the generation.
  • Property — a stale claim cannot clear or supersede the current one.
  • Quality attribute — correctness under concurrency; crash-safety.

Start with what the model means. A job is leased exactly when it has an owner; the two are the same fact seen from two sides, so the model represents ownership as the presence of a current claim rather than as a separate flag that could disagree with it. That is a definition, not a property that could fail. It sets up the invariant that can.

The consequential invariant is about time and contention. Suppose worker A holds the claim at generation 7, appears to stall, and is reclaimed; the job is re-leased to worker B at generation 8. If A now wakes and tries to release using its generation-7 claim, that release must not clear B's current generation-8 claim. The generation makes the distinction decidable: a release carrying an old generation names a claim that no longer owns, so it is inapplicable to the current one.

Figure 2.3-4 draws the claim and its lifetime; the generation is the small addition that separates a live claim from a stale one.

In-flight ownership: CLAIMED releases on completion or becomes reclaimable on expiry A claim opens the CLAIMED state, carrying owner, epoch, and expires_at. Two transitions leave it. Completion releases the claim to a RELEASED outcome. Expiry moves it to RECLAIMABLE, a lapsed state from which another actor may claim it again. The model distinguishes a live claim from a stale one and states when the window has lapsed, without representing the storage machinery that implements the lease. IN-FLIGHT OWNERSHIP claim CLAIMED owner · epoch · expires_at completion expiry RELEASED claim ends cleanly RECLAIMABLE lease lapsed / stale another actor may claim Completion releases the claim; expiry makes it reclaimable. A live claim is distinguishable from a stale one — expiry is a state, not an accident.
Figure 2.3-4. In-flight ownership model. A current claim records owner, epoch, and lifetime. Completion releases the claim; expiry makes it reclaimable. The model distinguishes a live claim from a stale one without representing the storage machinery that implements the lease.

The generation exposes the question — is this release applicable to the current claim? — and the model's job ends at making that invariant precise and checkable. Whether the release path holds the line is enforcement for Chapter 3: a hard guard that refuses the stale release rather than merely reporting it, with an exhaustive search over the interleavings serving as its verification.

Notice what this model omits: the processing topology. Ownership, generation, lifetime, and reclamation are the consequential properties for this question; how the job's work is partitioned is not. Indeed, the implementation changed over time in ways that optimized its performance but not its semantics. We changed the pointers to the code, but not the model.

FORMAL METHODS

Inset — What is an invariant?

An invariant is a property required to hold over a declared domain of states, structures, or observations. In a behavioral state machine, the invariant may be a predicate that must hold in every reachable state; in a structural model, it may require every observed dependency to belong to a declared set; in a measurement model, it may require a quantity to remain within a hard capacity bound. State both the property and the domain the checker claims to establish it over.

Take a behavioral illustration. A job carries two fields at once — a status of free, leased, or done, and a lease_owner that names the holding worker or is empty. At the model level, leased-iff-owner was a definition; an implementation that represents the two sides as separately written fields turns it into a property that can fail, which is exactly why you write the invariant down. "A job is leased if and only if it has an owner" is a predicate over the pair: (status == "leased") == (lease_owner is not None). A free status with a lingering lease_owner is a stale lease; a leased status with no owner is a lost lease. Separating the two writes can make either inconsistent state reachable, and both break the predicate. The predicate becomes mechanically meaningful when a checker evaluates it over the declared reachable state space:

STATES = product({"free", "leased", "done"}, {None, "worker-1", "worker-2"})
def invariant(s):                                    # leased iff owned
    return (s.status == "leased") == (s.lease_owner is not None)
assert all(invariant(s) for s in reachable_states())  # check every reachable state

2.3.5 One Representation, Several Questions

The lease is the chapter's clearest case of one representation answering several classes of question. Read it as an ownership model and it says who controls a job. Read the same claims as a behavioral model and they trace a lifecycle — claimed, held, expired, reclaimed. Count the active leases and the same representation becomes a measurement: how much work is genuinely in flight right now. Figure 2.3-5 sets the three readings side by side.

One shared lease state answers ownership, behavioral, and measurement questions A single shared lease state, carrying owner, epoch, and lifetime, sits at the top and fans down to three purpose-views: ownership, who owns it; behavioral, when is it stale; and measurement, how many are active. One represented state, several engineering questions. Model classes distinguish purpose, not storage objects. SHARED LEASE STATE owner · epoch · lifetime OWNERSHIP who owns? BEHAVIOR when stale? MEASUREMENT how many active? One represented state, several engineering questions.
Figure 2.3-5. Model classes overlap. The same lease state supports ownership, behavioral, and measurement questions. The classes distinguish purpose, not storage objects.

The overlap follows from the distinction introduced at the opening of the chapter: model classes identify engineering questions, not mutually exclusive data structures. One purposeful representation can answer several when they share the same underlying facts. This is the observation the closing section builds on when it connects the models through shared identity.

Ownership introduced permission implicitly: a stale claimant may not clear a current lease. The next family makes permission the whole question.

Works Cited

  1. Harel, David. “Statecharts: A Visual Formalism for Complex Systems.” Science of Computer Programming 8, no. 3 (1987): 231–74. https://doi.org/10.1016/0167-6423(87)90035-9.
  2. Baier, Christel, and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.
  3. Gray, Cary G., and David R. Cheriton. “Leases: An Efficient Fault-Tolerant Mechanism for Distributed File Cache Consistency.” In “Proceedings of the Twelfth ACM Symposium on Operating Systems Principles.” Special issue, Proceedings of the Twelfth ACM Symposium on Operating Systems Principles (New York), 1989, 202–10. https://doi.org/10.1145/74850.74870.
© James C. Davis, 2026–present