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¹1. 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).

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 checking²2. 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.

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 Part III. 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 Part III'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.

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, awaiting-merge, 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 chapter 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.