Formalizing System Requirements Using State Machines

In this lesson, you will learn how to translate ambiguous system requirements into deterministic, verifiable state machines to eliminate logic hazards in mission-critical embedded software.

When building reliable systems, human-readable requirements (like "the system should shut down on a fault") are often too vague to implement safely. By formalizing these requirements as Finite State Machines (FSMs), we replace "if-else" spaghetti code with a rigid structure that defines exactly how the system reacts to every possible input at any given time.

Why Formalize with State Machines?

An FSM consists of a finite number of states, transitions, and inputs. By mapping your requirements to a state transition table, you can mathematically prove that your system will never enter an "undefined" state. This is vital for safety, as it allows us to identify and handle "dead" states or unreachable code—classic sources of system instability.

Implementation Example

Consider a simple mission-critical heater controller. Instead of checking flags throughout your code, you define an enumeration and a transition function:

typedef enum { STATE_IDLE, STATE_HEATING, STATE_FAULT } SystemState;

SystemState current_state = STATE_IDLE;

void process_event(Event e) {
    switch (current_state) {
        case STATE_IDLE:
            if (e == START) current_state = STATE_HEATING;
            break;
        case STATE_HEATING:
            if (e == OVERHEAT) current_state = STATE_FAULT;
            else if (e == STOP) current_state = STATE_IDLE;
            break;
        case STATE_FAULT:
            // Fail-safe logic: only external reset can clear
            break;
    }
}

Verifiable Reliability

Because the FSM logic is structured, it becomes a target for formal verification. You can easily create a state transition matrix to ensure every combination of input and state has a defined outcome. If a transition is missing, you know immediately that your requirement specification is incomplete. Furthermore, this structure simplifies the implementation of "Safe Recovery Sequences" (Lesson 7) by ensuring that any error transition forces the system into a known, predictable state rather than an indeterminate software branch.

Key Takeaway: By modeling system logic as a formal state machine, you replace unpredictable branching with a deterministic, testable structure that is essential for proving the reliability of safety-critical embedded systems.