A state machine is a model of a system's behavior as 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 gives the states names and makes the transitions values, so 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, and the code follows it.
• Stateflow (MATLAB / Simulink; commercial) — 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.
• Erlang/Elixir: gen_statem (OTP, since Erlang/OTP 19).
• C/C++: Boost.MSM, Boost.SML.

State machines as plain typed code

• A language with sum types can encode a state machine as a sum type with a transition function. That needs no library and no DSL, and the compiler checks that every match covers every state. Elm, Rust, OCaml, Haskell, and TypeScript discriminated unions all fit this idiom.

Model-check the chart

• TLA+ / Alloy / SPIN — model checkers that explore a chart translated into their specification language, worth the translation when the state space is important enough.
• PRISM — probabilistic model checker for stochastic transitions (retry policies, backoff). See probabilistic 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); used in safety-critical avionics and rail.
• 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.
• TorXakis and JTorX do model-based conformance testing (ioco) against a labeled-transition-system spec.

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 of TLS (Ruiter and Poll 2015)², SSH (Fiterău-Broştean et al. 2017)³ and TCP (Fiterău-Broştean et al. 2016)⁴.

• LearnLib (JVM) and AALpy (Python) learn automata by active querying.

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 picks Harel statecharts as the fittest notation for UI state machines (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 support here is definitional rather than statistical: 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. Ruiter, Joeri de, and Erik Poll. 2015. "Protocol State Fuzzing of TLS Implementations." 24th USENIX Security Symposium (USENIX Security 15). https://www.usenix.org/system/files/conference/usenixsecurity15/sec15-paper-de-ruiter.pdf. ↩

3. Fiterău-Broştean, Paul, Toon Lenaerts, Erik Poll, Joeri de Ruiter, Frits Vaandrager, and Patrick Verleg. 2017. "Model Learning and Model Checking of SSH Implementations." Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. https://doi.org/10.1145/3092282.3092289. ↩

4. Fiterău-Broştean, Paul, Ramon Janssen, and Frits Vaandrager. 2016. "Combining Model Learning and Model Checking to Analyze TCP Implementations." Computer Aided Verification (CAV 2016), Lecture notes in computer science. https://doi.org/10.1007/978-3-319-41540-6_25. ↩

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