Note: This article discusses architectural patterns for composing finite state machines. While these principles inform safety-critical design, specific implementations require verification appropriate to their regulatory context.
The promise of modular software is straightforward: build small, verified components, then combine them into larger systems. The reality is often disappointing. Components that work correctly in isolation interact in unexpected ways. Properties that held individually disappear when modules connect. The system becomes less than the sum of its parts.
This failure mode is not inevitable. When components are designed with composition in mind—when their properties are structural rather than incidental—the resulting systems can inherit guarantees from their constituent parts. The key lies in understanding what makes composition safe.
The Composition Problem
Consider two well-tested modules: a heartbeat detector that tracks whether a system is alive, and a statistical baseline that monitors for timing anomalies. Each works correctly in isolation. Each has passing tests and verified invariants.
Now connect them. The heartbeat detector outputs inter-arrival times; the baseline detector consumes them. What properties does the combination have?
The honest answer, for most software, is “unclear.” The modules were designed independently. Their interaction creates a new system with emergent behaviour that neither module anticipated. Edge cases multiply. Timing dependencies appear. The composition may work, but you cannot know without testing every possible interaction—a combinatorial impossibility.
This uncertainty is the composition problem: connecting verified components does not automatically yield a verified system.
Why Most Composition Fails
The composition problem has deep roots. Most software modules are designed for convenience rather than composability. They carry implicit assumptions about their environment: that inputs will arrive in certain orders, that global state will be initialised, that timing constraints will be met. These assumptions work when a human orchestrates the modules carefully. They fail when modules are combined mechanically.
Consider a module that caches its last result for efficiency. In isolation, this optimisation is invisible—the module returns correct outputs. But when composed with another module that expects fresh computation on every call, the cached values create subtle errors. The caching assumption (that results can be reused) conflicts with the freshness assumption (that each call triggers new computation). Neither module is wrong; their assumptions are simply incompatible.
More formally, the problem is that modules have hidden state and hidden dependencies. They reach outside their defined interfaces to touch shared resources, timing mechanisms, or implicit contracts. These hidden channels create coupling that composition cannot see and therefore cannot verify.
Three Properties That Enable Safe Composition
The c-from-scratch project takes a different approach. Every module is designed from the start with three properties that, together, enable composition without compromise.
A module is closed if it depends only on its explicit inputs and internal state. No global variables. No hidden channels. No ambient dependencies.
Closure eliminates hidden coupling. A closed module can be reasoned about in isolation because there is nothing outside its interface that affects its behaviour. What you pass in, and what it contains, is all there is.
A module is total if it handles every possible input. No undefined behaviour. No assumptions about what inputs are "valid." Every state and every input has a defined response.
Totality eliminates edge-case failures. A total module cannot be surprised by unexpected inputs because it has a response to everything. When modules are composed, the output of one becomes the input of another—and that input is handled, regardless of what it contains.
A module is deterministic if the same state and input always produce the same next state and output. No randomness. No timing dependencies. No non-determinism.
Determinism eliminates interaction surprises. When you compose deterministic modules, the composite is also deterministic. The same sequence of inputs will always produce the same sequence of outputs, making the system testable and reproducible.
These three properties are not optional features. They are the mathematical requirements for composition that preserves guarantees.
A Concrete Example: The Timing Health Monitor
The c-from-scratch course builds toward a composed system: the Timing Health Monitor. It combines two FSMs—Pulse (for heartbeat detection) and Baseline (for anomaly detection)—into a single system that answers: “Is this process alive and behaving normally?”
The Pulse Component
The Pulse FSM tracks liveness using three states (as explored in Heartbeats and State Machines):
Pulse States: { UNKNOWN, ALIVE, DEAD }
Pulse Inputs: { BEAT, TIMEOUT }When a heartbeat arrives, Pulse transitions toward ALIVE. When too much time passes without a beat, Pulse transitions toward DEAD. The module outputs inter-arrival times (Δt) between consecutive heartbeats—this becomes the input to the next module.
The Baseline Component
The Baseline FSM monitors those inter-arrival times using exponential moving averages (see Statistics as State Transitions):
Baseline States: { LEARNING, STABLE, DEVIATION }
Baseline Inputs: { Δt (timing value) }During the LEARNING phase, Baseline accumulates statistics. Once sufficient data exists, it transitions to STABLE. If subsequent values deviate significantly from the established baseline, it transitions to DEVIATION.
The Composition
The composed Timing Health Monitor has four states:
Timing States: { INITIALIZING, HEALTHY, UNHEALTHY, DEAD }The mapping from component states to composed state is a pure function:
| Pulse | Baseline | → Timing |
|---|---|---|
| DEAD | (any) | DEAD |
| UNKNOWN | (any) | INITIALIZING |
| ALIVE | LEARNING | INITIALIZING |
| ALIVE | STABLE | HEALTHY |
| ALIVE | DEVIATION | UNHEALTHY |
This mapping has important properties. DEAD is absorbing—once the heartbeat is lost, nothing else matters. HEALTHY requires both existence evidence (ALIVE) and statistical evidence (STABLE). The composed state reflects a conjunction of component knowledge.
Why This Composition Works
The composition works because both Pulse and Baseline satisfy closure, totality, and determinism. Let’s trace why.
Closure is preserved because the composed system’s state is simply the pair of component states. There is no additional hidden state, no global variables, no ambient dependencies. The composition function (the mapping table) is itself closed—it depends only on its inputs.
Totality is preserved because the mapping table is complete. Every possible combination of Pulse state and Baseline state has a defined Timing state. When Pulse produces an unexpected state, the composition handles it. When Baseline produces an unexpected state, the composition handles it. The domain is the Cartesian product of component domains, and every element of that product has a defined output.
Determinism is preserved because the composition function is deterministic and both components are deterministic. Given the same component states, the mapping always produces the same composed state. Given the same inputs to each component, they always produce the same next states. Therefore, given the same initial state and input sequence, the composed system always produces the same final state.
This is not an accident. It is the direct consequence of designing components with these properties from the start.
The Composition Function
At each step, the composed system executes a straightforward algorithm:
timing_step(state, event, timestamp):
1. Compute Δt if we have a previous heartbeat
2. Feed event/timestamp to Pulse
→ Pulse updates its state
→ Pulse produces ALIVE/DEAD/UNKNOWN
3. If Δt is available, feed to Baseline
→ Baseline updates its statistics
→ Baseline produces LEARNING/STABLE/DEVIATION
4. Map component states to composed state
→ Apply the mapping table
→ Return INITIALIZING/HEALTHY/UNHEALTHY/DEADThe order matters: data flows from event through Pulse (which produces Δt) through Baseline (which consumes Δt) to the final state. This order is determined by the data dependencies, not arbitrary convention.
What Composition Buys You
When composition preserves properties, several engineering benefits follow.
Component-level verification transfers to the system. The invariants tested on Pulse and Baseline individually continue to hold in the composed system. If Pulse has an invariant “DEAD state is entered only after ALIVE was observed,” that invariant holds in the composition. You verify components once; the verification extends.
Debugging becomes tractable. When the composed system misbehaves, you can trace the failure to a specific component. Was the timing anomaly due to Pulse misclassifying a timeout, or Baseline miscalculating the z-score? The closed boundaries between components let you isolate faults.
System behaviour is reproducible. Given an initial state and an input sequence, you can replay the exact behaviour. This supports post-incident analysis, regression testing, and certification evidence. See Cryptographic Execution Tracing for how this property enables audit trails.
Complexity remains manageable. The composed system has 4 states, not 3 × 3 = 9. The mapping table deliberately collapses the product space into meaningful distinctions. You reason about HEALTHY or UNHEALTHY, not about the twelve possible state combinations.
The Algebra of Composition
There is a deeper structure here. Closed, total, deterministic FSMs form a category in the mathematical sense. The objects are FSMs; the morphisms are well-typed connections between them. Composition is associative: (A ∘ B) ∘ C = A ∘ (B ∘ C). There is an identity FSM that passes inputs unchanged.
This algebraic structure means you can compose arbitrarily. Build Pulse and Baseline into Timing. Compose Timing with another FSM that handles recovery. Compose that with an FSM that manages logging. At each stage, the properties are preserved, and the composed system remains closed, total, and deterministic.
This is why the title says “without compromise.” You do not sacrifice verification for modularity or modularity for verification. The properties are additive, not contradictory.
Practical Implementation
The c-from-scratch course implements this composition in pure C, following the Math → Structs → Code methodology. The composed structure contains the component structures:
typedef struct {
pulse_t pulse;
baseline_t baseline;
timing_state_t state;
} timing_t;The step function implements the algorithm described above, with explicit error handling for edge cases like division by zero (see The Zero-Variance Problem for why this matters).
Every function maintains the three properties:
- All inputs come through parameters; all outputs go through returns or output pointers
- Every input combination is handled, including invalid inputs
- Given the same state and input, the same output is produced
Contract tests verify these properties, not just happy-path behaviour. Fuzz testing with random input sequences confirms the invariants hold under conditions the developer did not imagine.
Implications for Safety-Critical Systems
This compositional approach aligns with regulatory requirements for safety-critical software. Standards like IEC 62304 and DO-178C emphasise modular design, traceability, and verification evidence. A system composed of verified components, with a verified composition, provides exactly the evidence these standards require.
The CardioCore kernel applies these principles to cardiac rhythm monitoring. The MDCP platform extends them to multi-core determinism. In both cases, the mathematical foundation—closed, total, deterministic FSMs that compose safely—is what enables certification-ready designs.
Conclusion
The composition problem is real: connecting verified components does not automatically yield a verified system. But it is solvable, when components are designed with composition in mind.
The key is structural: modules must be closed (no hidden dependencies), total (handle all inputs), and deterministic (same inputs produce same outputs). When components satisfy these properties, their composition inherits them. Verification extends from parts to whole.
This is not a theoretical nicety. It is a practical requirement for systems that must be trusted. When a pacemaker monitors cardiac rhythm, or an autonomous vehicle tracks its environment, or a satellite maintains its attitude, the composed system must work correctly—not just its individual pieces.
The c-from-scratch project teaches this approach from first principles: define the mathematics, transcribe to data structures, implement the step function, verify with contracts. The Timing Health Monitor is a concrete example of composition done right.
As with any architectural approach, suitability depends on system requirements, risk classification, and regulatory context. But for systems where correctness matters—where “probably works” is insufficient—composition without compromise is not optional. It is the engineering discipline that makes verification tractable.