Validating executable controller specifications through formal model checking

In many embedded control system applications, the control algorithm includes both logical and data flow portions. We apply formal methods of system verification to discrete-state algorithms. Specifically, we make use of a formal model checking tool to prove or disprove various properties of the algorithm. Questions pertaining to the achievability of states and paths and proper variable assignment are cast as logical assertions in computation tree logic (CTL), and evaluated using the model checker. In addition, we describe an approach for generating scenarios; that is, a sequence of inputs and parameters that will take a discrete-state system model through a given sequence. We present several examples illustrating various questions that the designer may wish to pose, and an appropriate CTL assertion for each