A state machine encodes a finite set of states and the legal transitions between them. A statechart (Harel's extension (Harel 1987)¹) adds hierarchy, history, and orthogonal regions, useful when the flat state set explodes. Making the state machine an explicit artifact that the code refers to changes what the compiler can enforce: the states have names, the transitions are values, the compiler can check exhaustiveness, and reviewers can read the machine without reading the implementation.

What it catches

• Illegal transitions. A PaymentRefunded event fired on an Unpaid order should be a compile-time error, not a 500. The state machine makes "what events are valid in which states" a type-checked question.
• Forgotten states. Adding a new state (e.g., PartiallyPaid) and forgetting to handle one of the events in that state is a reviewer-visible omission when the chart is in the repo.
• Implicit state in code that should have explicit states. Order-status enums that drift; payment-flow paths the code navigates by string comparison; UI screens whose enabled/disabled state depends on an undocumented combination of booleans. The chart names the states the code was navigating anyway.
• Drift between design and implementation. When the chart is the source of truth and the implementation is generated or consulted, divergence is a code bug, caught at the test that drives the implementation through the chart.
• Concurrent state in protocol code. Statecharts with orthogonal regions model "two things happening at once" in a way that flat state machines and ad-hoc booleans don't; verifying the interleavings between regions is a separate job for model checking.

What state machines do not catch: anything outside the transition graph. Logic inside a transition (the side effect, the persistence write, the network call) is unchecked by the chart; pair with property-based testing or contracts on the transition bodies.

Tools

Library-supported statecharts

• XState (TypeScript/JavaScript) — statechart library; visual editor; treats the chart as the source of truth, the code follows. Closest mainstream implementation of Harel statecharts.
• Stateflow (MATLAB / Simulink) — used in aerospace, automotive, and embedded-systems toolchains.
• SCXML (W3C) — state-chart XML standard; supported by Apache Commons SCXML and others.

Per-ecosystem state-machine libraries

• Rust: statig, state_machine_future, sm, rust-fsm.
• Go: looplab/fsm, qmuntal/stateless.
• Java/Kotlin: Spring Statemachine, Tinder StateMachine (Kotlin DSL).
• Python: transitions, python-statemachine.
• Elixir: gen_statem (OTP, since Erlang/OTP 19).
• C/C++: Boost.MSM, Boost.SML.

State machines as plain typed code

• Any typed language can encode a state machine as a sum type with a transition function. Often the cheapest path: no library, no DSL, exhaustive matching enforced by the compiler. Elm, Rust, OCaml, Haskell, and TypeScript discriminated unions all fit this idiom.

Model-check the chart

• TLA+ / Alloy / SPIN — when the state space is important enough, lift the chart into a model checker. See model checking.
• PRISM — probabilistic model checker for stochastic transitions (retry policies, backoff). See statistical model checking.

Verify the chart directly

Beyond a library, some tools analyze the chart itself: unreachable states, nondeterministic transitions, and temporal properties, checked statically over the model.

• Ansys SCADE (commercial): synchronous-language statecharts with formal verification and qualified code generation (DO-178C); the safety-critical avionics and rail toolchain.
• Simulink Design Verifier (commercial): proves properties and detects dead logic on Stateflow charts, and generates tests from them.
• itemis's statechart IDE (formerly Yakindu Statechart Tools) and IBM Rhapsody (both commercial): statechart / UML-state-machine authoring with model validation and code generation.

Generate tests from the chart

With the chart as the source of truth, model-based testing generates the tests that drive the implementation through it: each state and transition is a path to exercise.

• GraphWalker generates and walks test paths over an FSM model; AltWalker executes GraphWalker models against the implementation.
• fMBT (Intel) and ModelJUnit (JVM) generate sequences from a model.

Learn a chart from a black box

Active automata learning (Angluin's L*) recovers a chart from a system that has none: it infers an FSM by querying the implementation, and the inferred machine is then checked. It has been used to analyze protocol implementations (TLS, SSH, TCP).

• LearnLib (JVM) and AALpy (Python) learn automata by active querying.
• TorXakis and JTorX do model-based conformance testing (ioco) against a labeled-transition-system spec.

When to use, when not

Use:

• For any feature with a non-trivial lifecycle. Orders, payments, subscriptions, multi-step forms, dialog flows, document workflows.
• For UI components where enabled/disabled state depends on context: the chart makes that context explicit, and Wayne recommends it as the lightweight formal method for UI (Wayne 2018)².
• For protocol code at the application layer (HTTP retry/backoff state, connection lifecycle, cache state).
• When stakeholders need to read the flow. Statecharts are visual and approachable.

Don't:

• For simple toggles or two-state flows. The ceremony exceeds the value.
• For decision logic that doesn't have state. Use decision tables instead.
• For deeply concurrent or distributed protocols where the interleavings matter. Lift to model checking.

Evidence

The empirical literature on state machines as a practice (rather than as a formalism) is thin; the case rests on the definitional points: illegal transitions become type errors, forgotten transitions become visible omissions, and a mechanically checked chart cannot silently diverge from the code.

Classification

• Quality dimensions: Functionality.
• Area: UI flow control, order / payment / subscription lifecycles, protocol state, embedded control logic, asynchronous workflows, anything with explicit transitions.
• Guarantee: Exhaustive over the declared state × event space — every state and transition is enumerated, and illegal or forgotten transitions are rejected (compiler-checked, or model-checked over the transition graph).

Referenced by

• Automated test generation · Methods
• Decision tables · Methods
• Formal methods · Methods
• Temporal-logic falsification · Methods
• How AI fits into software quality · AI

References

---

1. Harel, David. 1987. "Statecharts: A Visual Formalism for Complex Systems." Science of Computer Programming 8 (3): 231–74. https://doi.org/10.1016/0167-6423(87)90035-9. ↩

2. Wayne, Hillel. 2018. Formally Specifying UIs. https://www.hillelwayne.com/formally-specifying-uis/. ↩