Collin Spencer: SF2SMV: Model Checking for Stateflow Diagrams with Floating Point Variables and Complex Expressions

Abstract: In general, statecharts are more complicated state machines. Stateflow, the MATLAB version of statecharts, includes hierarchy, events, state actions, and general arithmetic expresions involving floating point variables. With the extra complexity, Stateflow diagrams are difficult (if not impossible) to test exhaustively. Given a finite number of floating point values as inputs, however, a Stateflow diagram will typically produce a finite set of output values. If this condition holds, then a Stateflow diagram with complicated expressions and floating point variables can be represented in a finite state model checker such as SMV. SF2SMV is a MATLAB-based tool that implements this approach to verifcation of Stateflow diagrams.

Biography: Collin Spencer is a MS student currently working in statechart verification at Carnegie Mellon University.