Verifying System Properties with Model Checking

Use model checking tools to exhaustively verify that your state machine design satisfies safety properties like deadlock avoidance and liveness.

In this lesson, you’ll learn how to use model checking to mathematically prove that your state machine designs are free of deadlocks and guaranteed to reach critical safety states.

While testing (like fault injection) verifies that your code behaves as expected under specific scenarios, model checking verifies that it cannot behave in any way that violates your safety requirements across all possible execution paths. By treating your state machine as a mathematical graph, a model checker exhaustively traverses every reachable state to ensure no "forbidden" condition is ever met.

The Verification Process

To verify a system, you express your design as a formal model (using a language like Promela for the tool SPIN) and define your safety properties using Linear Temporal Logic (LTL).

Consider a simple DoorController state machine. You want to ensure two things:

Safety: The door is never open when the vehicle is in motion (Deadlock/Violation avoidance).
Liveness: If a "close" command is issued, the door eventually reaches the CLOSED state.

You translate your state machine into a set of transitions:

// Formalized state transition in model logic
active proctype DoorController() {
    do
    :: (state == OPEN && motion == TRUE) -> assert(false); // Safety Property
    :: (state == CLOSING) -> state = CLOSED;              // Liveness Path
    :: (state == CLOSED && cmd == OPEN) -> state = OPEN;
    od
}

The model checker explores every combination of state, motion, and cmd variables. If it finds a path where the assert(false) is triggered, it provides a counter-example—a step-by-step trace showing exactly which sequence of inputs leads to the hazardous state.

Why this matters for Embedded Systems

In embedded systems, concurrency bugs or complex state interactions often hide in rarely executed branches. Traditional testing might miss these because they require precise, obscure input timing. Model checking eliminates the need for "luck" in testing by analyzing the entire state space of your logic, ensuring that your system design is robust before a single line of C code is even written.

Key Takeaway: Model checking moves verification from "probing for errors" to "proving the absence of errors" by exhaustively exploring all possible state transitions in your design.