Recursive Modeling of Stateflow as Input/Output-Extended Automaton

Stateflow, a graphical interface tool for Matlab, is a common choice for design of event-driven software and systems. In order for their offline analysis (testing/verification) or online analysis (monitoring), the Stateflow model must be converted to a form that is amenable to formal analysis. In this paper, we present a systematic method, which translates Stateflow into a formal model, called Input/Output Extended Finite Automata (I/O-EFA). The translation method treats each state of the Stateflow model as an atomic module, and applies composition/refinement rules for each feature (such as state-hierarchy, local events) recursively to obtain the entire model. The size of the translated model is linear in the size of the Stateflow chart. Our translation method is sound and complete in the sense that it preserves the discrete behaviors as observed at the sample times. Further, the translation method has been implemented in a Matlab tool, which outputs the translated I/O-EFA model that can itself be simulated in Matlab.