# SL2SF: Refactoring Simulink to Stateflow

## Abstract

In the Matlab Simulink environment, systems can be modelled using Simulink block diagrams and Stateflow state charts. While stateful logic is more naturally modelled using Stateflow, in practice complex block diagrams are often used instead, resulting in models that are hard to understand and maintain. In order to improve the maintainability and understandability of large industrial models, this paper presents a strategy for refactoring Simulink block diagrams implementing stateful logic into functionally equivalent Stateflow state charts that more naturally represent the intended behaviour. To bridge the gap between the syntax of block diagrams and state charts, Mealy machines represented by tabular expressions are used as an intermediate representation. The compositional language of block diagrams is used to combine tables modelling individual blocks into a table for the entire block diagram which describes the high level state machine encoded in the Simulink subsystem. A prototype tool that performs the translation from Simulink to Stateflow automatically is discussed.

## Keywords

Simulink Stateflow Refactoring Mealy machines Tabular expressions Monoidal categories## 1 Introduction

The adoption of Model-Based Design in the development of embedded control systems across industries has led to the wide use of Matlab/Simulink/Stateflow as a supporting environment. The modelling capabilities provided by Simulink block diagrams and Stateflow state charts complement each other by providing languages for functional and stateful system specifications. Due to their individual strengths, one modelling formalism may be preferable for specifying certain classes of behaviours. For example, the MathWorks Automotive Advisory Board (MAAB) guidelines [25] advise the use of Stateflow over Simulink for modelling stateful logic. This is because Simulink block diagrams that are used to model mode switching logic are often cumbersome and difficult to understand. In this case, Stateflow state charts should be used to implement the same logic resulting in a structure which is easier to read, maintain, and verify.

*exit*actions of the mode it is leaving, the actions on the transition it is taking, and the

*entry*actions of the mode it is entering. If no transitions are valid, the state chart remains in its current mode and executes the

*during*actions of that mode.

The Simulink and Stateflow models shown in Fig. 1 are functionally equivalent. Both models capture a timer with one boolean input, \( start \), and one boolean output, \( running \). When \( start \) becomes true, the system starts counting down from ten to zero. While the system is counting down, \( running \) is true. Once the counter reaches zero, \( running \) is set to false and becomes true again if \( start \) is true. Although there are relatively few blocks in Fig. 1a, it is difficult to understand how this model achieves the behaviour while the state chart in Fig. 1b clearly captures the system’s modes and the conditions triggering mode changes.

Our industrial experience has identified the need to refactor Simulink block diagrams to Stateflow state charts for easier comprehension and maintenance. More precisely, practice shows that Simulink is often used to specify stateful logic even though Stateflow would be a more appropriate implementation language. This might occur during model evolution when modes of operation are added to previously mode-free block diagrams, and developers find it easier to modify the existing Simulink logic to accommodate the change than to reproduce the behaviour from scratch in a state chart. Other times, a developer’s preference dictates the choice of modelling formalism. Manual refactoring from Simulink to Stateflow, although feasible, is a time consuming and error prone process which requires that the behaviour of complex Simulink models is completely understood.

This paper presents an approach to translate block diagrams into behaviourally equivalent state charts. The approach converts individual blocks into tabular expressions [21] to expose their latent state variables and decision logic. The data flow between blocks is then used to combine tables into a single, larger table describing the entire block diagram. Then, the elements of state charts (states, transitions) are identified by reconfiguring the combined tables into a form similar to state charts. Behavioural equivalence is established by giving semantics to block diagrams, state charts, and the intermediate tables as Mealy machines. The paper’s main contributions are: (i) A method for translating Simulink block diagrams to Stateflow state charts via tabular expressions. (ii) A categorical framework for composing Mealy machines by combining their update functions as the basis of the translation. (iii) A prototype tool implementing the translation from Simulink to Stateflow.

This paper is organized as follows. Section 2 describes how we model systems and our categorical framework for combining them. Section 3 illustrates the translation method with a simple example. Section 4 describes the application of the categorical framework to convert block diagrams to tabular expressions. Section 5 explains how tabular expressions are converted to state charts. Section 6 describes the prototype tool. Related work is covered in Sect. 7 and the paper concludes with Sect. 8.

## 2 Background: Modelling Systems and Their Combinations

This section describes the formalisms underlying the proposed translation approach: Mealy machines, tabular expressions, and monoidal categories.

### 2.1 Mealy Machines: Modelling Stateful Systems

To preserve behaviour, the semantics of both block diagrams and state charts are modeled using *Mealy machines*.

### Definition 1

*A* Mealy Machine *m* is a tuple \((S, s_0, \varSigma , \varLambda , ud)\), where *S* is a set of states (the *state space*), \(s_0 \in S\) (the *initial state*), \(\varSigma \) is a set of input values (the *input alphabet*), \(\varLambda \) is a set of output values (the *output alphabet*), and \(ud : \varSigma \times S \rightarrow \varLambda \times S\) is a function (the *update function*) which computes the current output and next state from the current input and current state.

For example, the unit delay \(\frac{1}{z}\) block labelled \(counter\) in Fig. 1a can be modelled as the Mealy machine \( delay = (\mathbb {R},0,\mathbb {R},\mathbb {R}, shift )\). The block has an input variable (port) *i*, an output variable (port) *o*, and an internal state variable \( counter \), where \(i,o, counter \in \mathbb {R}\). When the block updates, it outputs the current state value \(o = counter \), and updates the state to store the current input value \( counter ' = i\), i.e. \((o, counter ') = shift (i, counter )\), where \( shift : \mathbb {R}^2 \rightarrow \mathbb {R}^2\) is defined as \( shift (i, counter ) = ( counter , i)\).

While Simulink has no formal semantics, our use of Mealy machines to model their behaviours is consistent with the informal semantics described in Chap. 3 of the Simulink User Guide [26].

### 2.2 Tabular Expressions: Representing Conditional Behaviours

*horizontal condition tables*(HCTs) as presented in [28]; and

*state transition tables*(STTs), which specialize HCTs to describe state charts similarly to the ones presented in [24].

An HCT is represented in Fig. 2a. It is a tabular representation of the update function of a Mealy machine which models the block diagram from Fig. 1a. Given the variable values \( start = true\) and \( counter = 0\), the table can be evaluated from left to right in the following way. Since the first condition \( start \) of the first column is satisfied, and the sub-condition \( counter \le 0\) in the second row of the second column is satisfied, we use the second row to determine that \( running \) is given the value of \( false \), and \( counter '\) is given a value of 10.

The second tabular representation, STTs, are also used to represent the update function of Mealy machines. Their special format closely matches the state charts they model. For example, the STT in Fig. 2b represents the state chart in Fig. 1b. Each mode is listed in the first column, and the condition of each transition is listed in the second column, adjacent to the mode they leave. The columns after the double bars describe how each output/state variable is updated by the actions of the associated transition. The final column of each row indicates which mode the associated transition leads to.

Tabular expressions were given a precise semantics in [10]. The structure of tables can be rearranged without changing the function they describe, e.g., conditions can be reordered as in [4]; conditions can be combined with sub-conditions (via conjunction) to flatten the hierarchy of conditions; and normal expressions in the table can be simplified by assuming the conditions to their left hold.

### 2.3 Categorical Framework: Combining Systems

The key idea of block diagrams is to combine simple, predefined blocks to describe a behaviour. The language of *monoidal categories* explains how to break down the complex data flow of block diagrams and describe it in terms of simpler data flow [5] (i.e. cascading blocks in sequence, placing blocks in parallel, and feeding outputs of blocks back to their inputs).

*morphisms*. Simple data flow constructs are described as operations on morphisms, which can be visualized using block diagrams called

*string diagrams*[5, 22]. In this section, we discuss the wiring constructs in the concrete setting of the category

**Set**, where morphisms are functions from an input set of tuples to an output set of tuples (called the

*domain*/

*codomain*

*objects*of the morphism).

A fragment of the block diagram from Fig. 1a can be used to illustrate the idea behind the basic data flow operations. The string diagram in Fig. 3 describes a function that is broken down into sub-functions combined via two operations: sequential combination (denoted “; ”) and parallel combination (denoted “\(\otimes \)”). The fragment describes a function *g* from \(\mathbb {R} \times \mathbb {B}\) to \(\mathbb {R}\). Each wire extending from the left/right of the large compound function indicates an input/output value, respectively. The wire is labelled with the set from which the value comes. If there are multiple wires, the domain or codomain of the function is given as the Cartesian product of those sets. In monoidal categories, the Cartesian product is generalized as an operation called the *monoidal product on objects*.

The function *g* is composed of a sequence of sub-functions, \(g = f_1 ; f_2 ; f_3 ; f_4\). The sub-functions (except for \(f_4\)) consist of functions composed in parallel with wires and other functions. The wiring “data routing functions” are then defined as follows: a normal wire is the *identity* function \(\mathrm {id}_X = \{(x) \mapsto (x)\}\); wires crossing over each other define the *braiding* function \(\mathrm {Br}_{A,B} = \{(a,b) \mapsto (b,a)\}\); and branching wires are called the *diagonal* function \(\varDelta _X = \{(x) \mapsto (x,x)\}\). The functions are indexed with the set(s) over which they are defined. Morphisms like these functions have special status in monoidal categories and must satisfy some axioms to verify that they “act like wiring” in the host category.

Sub-function \(f_3\) can now be described as \(f_3 = add \otimes \mathrm {id}_{\mathbb {R}} \otimes \mathrm {id}_{\mathbb {R}}\). Functions combined in parallel have domains/codomains which are the Cartesian products of the domain/codomain of the component functions. The parallel combination uses each component function independently to calculate each component of the output. For example, taking \(add = \{(x_1,x_2) \mapsto (x_1 + x_2)\}\), the function \(add \otimes \mathrm {id}_{\mathbb {R}} \otimes \mathrm {id}_{\mathbb {R}}\) is given by \(\{(x_1, x_2, x_3, x_4) \mapsto (x_1 + x_2, x_3, x_4)\}\). In monoidal categories this operation is generalized as the *monoidal product on morphisms*, where the domain/codomain of a product morphism is given by the monoidal product of the domain/codomain objects of the component morphisms. It is notable that we can also describe sub-function \(f_3\) as \(f_3 = add \otimes \mathrm {id}_{\mathbb {R}^2}\), where the two wires are treated as one function. This is useful, for example, when describing the sub-function \(f_2\) as \(f_2 = \mathrm {Br}_{\mathbb {R}^2, \mathbb {R}} \otimes sw _\mathbb {B}\).

Describing \(f_1\) requires modelling constant blocks as functions. Therefore, constants are described as functions with inputs from the singleton set \(\mathbbm {1} = \{()\}\), and we draw functions with domain/codomain \(\mathbbm {1}\) as blocks with no wires extending from the left/right side, respectively. Functions modelling constant blocks, \([k] = \{() \mapsto (k)\}\), always take the empty tuple as input, and always produce the same value *k* as output. The function \(f_1\) can now be described as \(f_1 = \varDelta _\mathbb {R} \otimes [-1] \otimes [10] \otimes \mathrm {id}_{\mathbb {B}} \otimes [0]\). Objects like \(\mathbbm {1}\) have special status in monoidal categories and are called the *monoidal unit*. Taking their monoidal product with any other object *X* yields the same object *X*. Intuitively, this means that concatenating any tuple \((x_1, .., x_n)\) with the empty tuple () does nothing. This explains why the product of the domains of the functions in \(f_1\) is the set \(\mathbb {R} \times \mathbbm {1} \times \mathbbm {1} \times \mathbb {B} \times \mathbbm {1}\), but the domain of \(f_1\) is described as \(\mathbb {R} \times \mathbb {B}\)—the former simplifies to the latter.

*g*in terms of simple data flow:

*x*exists for each \(a \in A\), the loop configuration is considered

*well-formed*. Following [11], we encode the addition of such loops with a

*trace*operation: \(\mathrm {Tr}_{A,B}^{X}(f) = f^{*}\).

*fixed point equations*to specify traces, which is generalized by the approach from [8]. Since these fixed point equations are not guaranteed to have a unique solution, the trace operation is

*partial*—it is only defined for loop configurations that are well-formed. Partial traces have been described in [15], and the guarded structure introduced in [7] compositionally describes which feedback configurations are valid. For the loops to “act like wiring”, certain axioms must be satisfied, e.g., the

*yanking*axiom (as shown in Fig. 4b) states that \(\mathrm {Tr}_{X,X}^{X}(\mathrm {Br}_{X,X}) = \mathrm {id}_X\) for any set

*X*.

## 3 Translation Strategy

The translation strategy is composed of three steps. This section illustrates these steps by considering the example from Fig. 1.

First, the decision logic implemented by the block diagram is encoded as the HCT in Fig. 8a. This step is described in Sect. 4. In the second step, the representation is simplified as, depending on the value of \( counter \), only some rows of the table can be valid. By associating a certain range of state variable values with a mode of operation, we simplify the representation by considering only the conditions which are possible. This allows us to leverage the conditions from HCTs to determine the modes of operation by rearranging HCTs into equivalent STTs such as Fig. 2b. The final step trivially rearranges the information from STTs into a state chart by creating a transition for each row. The conversion from HCTs to STTs to state charts is described in Sect. 5, and possible simplifications to the resulting state chart are discussed.

Even with such a simple example, the importance of automated refactoring becomes apparent. If the model were to be refactored manually, a state chart that is not equivalent to the block diagram could be created unintentionally. For example, one can manually produce a state chart that transitions out of the \( Running \) mode when \( counter \) is zero, rather than one.

## 4 Block Diagrams to HCTs: Mealy Composition

The first step of the translation strategy is to model the entire block diagram as a Mealy machine whose update function is represented as a HCT. To achieve this, Simulink block diagrams are modelled in a category **Mealy**, where morphisms (i.e. blocks) are Mealy machines, not functions. We then show how the update functions of composite Mealy machines built from the operations described in Sect. 2.3 can be built from the update functions of the component Mealy machines using the same operations on functions. Then, the predefined update functions of individual blocks can be represented using HCTs and combined according to the functional combinations derived from the block diagram.

### 4.1 Mealy Machines and Their Combinations via Functions

In this section, we consider a category **Mealy** whose objects are sets, and whose morphisms \(m : \varSigma \rightarrow \varLambda \) are Mealy machines with input alphabet \(\varSigma \), and output alphabet \(\varLambda \). Composition of morphisms is given by the usual definition of cascade composition of Mealy machines [13]. We also introduce a monoidal product, giving the category a monoidal structure. It is defined on objects as the Cartesian product of sets, and on morphisms as the parallel composition of Mealy machines. The unit of the monoidal product is the same as for sets, the set containing one element: \(\mathbbm {1}\). Considering equality of morphisms up to bisimilarity results in a structure similar to the one used in [9] to describe symmetric lenses—according to [9], this structure forms a (symmetric) monoidal category.

*m*can be expressed using the projection mapping Open image in new window . For update functions, the string diagram is decorated with grey backing to group the inputs/outputs of the update function into two main components: the upper components describe the inputs/outputs to the Mealy machine, and the lower components describe the current/next state (e.g. Fig. 5d).

**Set**. A Mealy machine \(m = (S, s_0, \varTheta \times \varSigma , \varTheta \times \varLambda , ud)\) can be traced to form the machine \(\mathrm {Tr}_{\varSigma , \varLambda }^{\varTheta }(m) = (S, s_0, \varSigma , \varLambda , ud')\) where the update function \( ud' \) is defined as Open image in new window as illustrated by Fig. 5f. Since this operation is defined in terms of traces in

**Set**, many of the properties of traces can be derived from traces in

**Set**.

The above results mean that if we know the update functions of individual Simulink blocks, then we can model the update functions of block diagrams which configure those blocks in sequence, in parallel, and with feedback.

### 4.2 Functional Embedding and Wiring Morphisms

In this section, we address the fact that a large part of a Simulink block diagram *looks* very functional (i.e. stateless). For example, many of the blocks and wiring in Fig. 1a can be modelled as functions. For this reason, we consider a class of Mealy machines which produce outputs as a function of only their current inputs. Any function \(f : X \rightarrow Y\) can be described as the Mealy machine \(\mathcal {M}f= (\mathbbm {1},(),X,Y,f)\), with one state, and update function *f* (see Fig. 6a). The mapping \(\mathcal {M}\) *embeds* morphisms from **Set** into the category **Mealy**, because any two embedded functions \(\mathcal {M}f\) and \(\mathcal {M}g\) interact in **Mealy** very similarly to the way they interact as functions in **Set**.

This explains how functional aspects of Simulink block diagrams can be modelled with Mealy machines. For example, the block labelled \( Mode \) in Fig. 1a can be modelled with the Mealy machine \(\mathcal {M}\textit{sw}_\mathbb {R}\). Perhaps more importantly, the morphisms introduced to describe wiring in functional diagrams (i.e. \(\mathrm {id}_{X}\), \(\varDelta _X\), \(\mathrm {Br}_{A,B}\)) can again be used to describe the same (functional) wiring for Mealy machines. Therefore, in string diagrams representing Mealy machines, plain wires represent the morphism \(\mathcal {M}\mathrm {id}_{X}\) which carries data without changing it, branching wires represent the morphism \(\mathcal {M}\varDelta _X\) which duplicates data, and crossing wires represent the morphism \(\mathcal {M}\mathrm {Br}_{A,B}\) which reorders the components of data. The fact that \(\mathcal {M}\mathrm {id}_{X}\) and \(\mathcal {M}\mathrm {Br}_{A,B}\) “act like wiring” is established in [9].

This establishes how to model wiring and functional blocks in Simulink block diagrams as Mealy machines. We can now use the operations from Sect. 4.1 to describe block diagrams which use complex wiring and functional blocks in combinations with stateful blocks.

### 4.3 Block Diagrams to Horizontal Condition Tables

**Mealy**, and related it to the same structure in

**Set**. This framework allows us to combine update functions of individual blocks into update functions of entire block diagrams using the above definitions. For example, the update function Open image in new window of the machine from Fig. 6b is equal toas shown in Fig. 6c, where the “\(\mathbbm {1}\)” wire is drawn in grey to illustrate how it achieves the data flow described by Fig. 5d (normally, this wire is not drawn). This can be simplified, e.g., the final sequential sub-function \(\mathrm {id}_\mathbb {R}\otimes \mathrm {Br}_{\mathbb {R}, \mathbbm {1}}\) is given by \(\{(x,(y,())) \mapsto (x, ((),y))\}\) which simplifies to \(\{(x,y) \mapsto (x,y)\}\) by flattening tuples. Our presentation of monoidal categories skips the formalities which describe this simplification, but it can be intuitively understood by considering the data flow described in Fig. 6c if the grey wire were absent (as usual). Taking Open image in new window (as defined in Sect. 2.1) which we now describe as \(\mathrm {Br}_{\mathbb {R}, \mathbb {R}}\) and using Open image in new window along with appropriate axioms over the wiring morphisms, Open image in new window simplifies to \((sw_\mathbb {R}\otimes \mathrm {id}_\mathbb {R}) ; \mathrm {Br}_{\mathbb {R}, \mathbb {R}}\). This simplification can be intuitively understood by considering only the black data flow in Fig. 6c. In the same way that we describe the functional data flow of Fig. 3, this approach can be repeated to describe the entire block diagram in Fig. 1a, not just the combination of blocks labelled \(Mode\) and \(counter\).

As mentioned in Sect. 2.3, not all feedback configurations are valid. The validity of a feedback configuration describing a Mealy machine is decided by determining whether or not the trace on its update function is defined. In many settings, the trace is defined if the aforementioned fixed-point equations have a unique solution [13]. However, for Simulink models that are used to generate embedded software, the configuration must satisfy a more strict validity condition: there must be no *algebraic loops*. This means there can be no cyclic dependencies in the underlying update function, any feedback can be trivially removed by rearranging the components and wiring to “yank out” the loops while preserving the connections between blocks. For example, Fig. 7 illustrates how the update function of a simple feedback configuration can be rearranged to remove loops. This can be formalized by the notion of vacuous guardedness introduced in [7].

HCTs—being representations of functions—can be composed like functions. We modify the composition operation in [20] to describe HCTs so that we can compose predefined tabular expressions as stated above. When composing two HCTs sequentially, the conditions of the first HCT appear first in the composed HCT and the conditions of the second HCT are included as sub-conditions. The conditions from the second HCT are evaluated using the output values from the first one. Consider, for example, the composition of Fig. 8a with Fig. 8b, where the output \( counter' \) of the first table is routed to the input \( counter \) of the second (ignore the \( running \) output for now). Their composition is shown in Fig. 8c (ignore the \( running \) and \( counter' \) outputs). The conditions \( counter >0\) and \( start \) (and their complements) appear in the same configuration as the first HCT. However, the sub-conditions (e.g. \( counter - 1 \le 0\)) come from the conditions (\( counter \le 0\)) in the second HCT, evaluated with the values (\( counter \mapsto counter - 1\)) from the row in the first HCT associated with the parent condition (\( counter > 0\)). The conditions \(10 > 0\) and \(0 > 0\) (and their complements) are generated in a similar manner, but because they are trivially satisfied/impossible conditions, the sub-conditions/entire row can be removed (the removable conditions/rows are shaded in Fig. 8c).

*mode*are constants, therefore they appear unchanged in Fig. 8c. For HCTs composed in parallel, the conditions from the second HCT are once again used as sub-conditions, but they are not modified. Similarly, the output expressions from both HCTs are placed in the combined table unchanged.

The predefined HCTs representing each function in the equation above can be combined using the operations described above to achieve a tabular expression for the entire block diagram. For example, the tabular expression in Fig. 2a can be obtained this way.

## 5 HCTs to STTs: Modes via Tables

The HCTs produced using the technique described in Sect. 4 are an intermediate representation in our translation strategy. They illustrate the decision logic of the system as a whole, but the logic is not related to state the way it is for state charts, i.e., through modes. This section explains how HCTs are augmented with modes to form STTs, and finally state charts.

### 5.1 Defining Modes

The STTs described in Sect. 2.2 have obvious similarities to state charts, but they are just syntactic sugar for HCTs. STTs and state charts are modelled as Mealy machines with a special state variable \( mode \) with values from an enumerated set *M* (see, e.g., extended state machines in [2]). The cells in the first column of STTs (see Fig. 2b) express conditions of the form \( mode = Running \) which compare the value of \( mode \) to each element of *M*. The last column identifies the updated value of \( mode '\). Therefore, the state spaces of Mealy machines modelling STTs and state charts have the form \(Q = S \times M\), where *M* is the set of modes, and *S* contains tuples of the other state variable values.

A HCT produced via the techniques in the previous section describes the update function *ud* of a Mealy machine \(m = (S, s_0, \varSigma , \varLambda , ud)\). We will enhance *m* with a state variable *mode* to produce a Mealy machine \(m^+ = (S \times M, (s_0, mode _0), \varSigma , \varLambda , ud^+)\) whose update function is given by a HCT which matches the format of an STT. To achieve the goal of improving readability, we leverage the existing decision logic in HCTs.

When a state chart updates, it only considers the transitions leaving its current mode, i.e., depending on its *state*, only some behaviours are possible. The same dependence on state is expressed in HCTs by conditions which depend only on the values of state variables, which will be referred to as *state conditions*. For example, in Fig. 8a, if the condition \( counter > 0\) is satisfied, the system can only do one thing: decrement \( counter \) and set *running* to true. Our strategy associates the condition \( counter > 0\) with a mode of operation \(Running \in M\), and replaces the original condition with \(mode = Running\). We augment the HCTs into STTs in a way that preserves the behaviour of the Mealy machines.

As the modes are all listed in the first column of an STT, the first augmentation reorders conditions in HCTs so that the state conditions appear first. For example, the conditions in Fig. 2a can be rearranged via the methods in [4] to obtain Fig. 8a. While our example contains only one pair of state conditions, HCTs describing general block diagrams may contain multiple nested state conditions. The second augmentation uses conjunction to flatten nested state conditions into a single column with a condition for each branch of the stateful logic.

The augmented HCT now has a specific form (Fig. 8a) which superficially resembles an STT, but the behaviour is unchanged. We now introduce a set of modes *M* with each element associated with a distinct condition in the first column of the augmented HCT. This association is defined by a function \( md : S \rightarrow M\) which maps tuples of state variable values to the mode whose associated state condition is satisfied. This function is represented by an HCT with the state conditions from the augmented HCT, and distinct values from *M* as outputs. The *md* function for the timer example is given by the HCT in Fig. 8b.

Next, the Mealy machine is enhanced by introducing a state variable *mode* with values from *M*. We design the enhancement to maintain the invariant that the value of \( mode \) always corresponds with the state condition which the other state variables satisfy. The invariant is satisfied by the initial state \((s_0, md (s_0))\). The enhanced update function trivially preserves the original behaviour by ignoring the value of \( mode \), but updates \(\textit{mode}'\) to maintain the invariant by evaluating *md* with the updated state variable values. The update function is therefore defined as \(ud^{+} = (ud \otimes !_M) ; (id_{\varLambda } \otimes (\varDelta _S ;(id_{S} \otimes md)))\), where \(!_M : M \rightarrow \mathbbm {1}= \{(\textit{mode}) \mapsto ()\}\) introduces an input whose value is discarded. Since *ud* and *md* are given as HCTs (e.g. Fig. 8a and b), the enhanced update function can be achieved through composition of tables (e.g. Fig. 8c).

This enhanced Mealy machine operates within a subset of the state space \(S \times M\) where the aforementioned invariant holds. The validity of any state condition can now be deduced from the value of the mode variable (e.g. \(( counter > 0) \Leftrightarrow (mode = Running)\)). Thus, replacing those conditions with the corresponding modes in the HCT representation of \(ud^+\) does not modify its behaviour. This is the final step in rearranging the HCT from Fig. 8c into the STT in Fig. 2b.

### 5.2 Converting to State Charts and Simplifying

The state chart in Fig. 9 implements the STT in Fig. 2b by creating a transition for each row and by creating assignment actions to update state and output variables. State charts produced in this manner can often be simplified by moving common actions from transitions to *entry* / *exit* actions of modes, or by removing transitions and performing the corresponding actions as *during* actions. For example, the state chart in Fig. 9 simplifies to the one in Fig. 1b.

In the example given above, it is crucial that the new state variable *mode* is tracked in addition to the existing variable \( counter \). The *mode* variable tracks the high level system state, but the \( counter \) variable is still important for tracking the detailed system state. This additional information is not always important, i.e., sometimes the mode is sufficient and the old state variable may be removed from the description of the Mealy machine. This may happen if a Boolean state variable generates a state condition; knowing the value of *mode* can be sufficient to deduce the value of the original state variable. It is also possible that a state variable from the block diagram stores more detailed information than necessary, and knowing the mode is sufficient for the state chart to act. In these cases, the unnecessary state variables can be removed from the state chart.

## 6 Prototype, Evaluation, and Future Work

The methodologies presented here have been used to develop a prototype tool which automatically refactors Simulink model fragments to Stateflow [18]. The tool supports a large subset of discrete Simulink blocks typically used for implementation of embedded software. The refactoring tool is implemented in Matlab and integrates with Simulink allowing the user to select the blocks they would like to replace. When the tool is invoked, it generates a Stateflow chart and uses the Simulink Design Verifier [17] to verify that it is equivalent to the selected blocks.

We also recognize the importance of finding refactorable fragments in large models. In fact, the translation methodology presented in this paper was developed in parallel with an identification strategy that pinpoints block diagrams which are candidates for refactoring—it searches for certain patterns of logical and stateful blocks which indicate complex state update logic. An elaborated description of both translation and identification strategies will be presented in the master’s thesis of the first author [29].

## 7 Related Work

Several papers propose translating Simulink block diagrams to formal languages to enable their verification using existing tools (e.g., [1, 6, 14, 23, 27, 30]). Only a few, however, translate Simulink block diagrams to state transition diagrams. In [19], Simulink block diagrams are converted into an extended version of hybrid automata, with each block in a block diagram converted to a hybrid automaton, leading to an explosion in the number of states of the resulting model. In [31], Simulink models are converted to finite state machines, but transitions between states represent the small execution steps of individual blocks updates, not changes in the high level system modes. Both studies [19, 31], as well as [16], do not aim to capture the high-level state machine of an entire block diagram. This is exactly what our approach does, with maintainability of the resulting model as a prime motivator.

Our approach to modelling Mealy machines and their interactions using the monoidal category **Mealy** follows a general trend in behavioural modelling. For example, monoidal categories have been used to describe interactions of quantum processes [5], labelled transition systems [12], and control systems [3]. The algebra of (traced symmetric) monoidal categories is similar to the algebra used to describe block diagrams in [6], but our approach uses a standard mathematical framework with a rich history and many known results. For example, the results of [9] indicate that by considering equivalence up to bisimilarity, the category **Mealy** is symmetric monoidal, meaning the appropriate axioms and resulting properties of this structure are already known.

## 8 Conclusion

In this paper, we proposed a method for translating Simulink block diagrams to Stateflow state charts via tabular expressions representing their respective Mealy machines update functions. A categorical framework for composing Mealy machines provides a theoretical basis for the translation. To the best of our knowledge, this is the first method for Simulink to Stateflow translation. Our proposed method is relevant to industrial development where it can help improve software maintainability and aid compliance with modelling guidelines.

## References

- 1.Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. Electron. Notes Theor. Comput. Sci.
**109**, 43–56 (2004)CrossRefGoogle Scholar - 2.Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)Google Scholar
- 3.Baez, J.C., Erbele, J.: Categories in control. Theor. Appl. Categories
**30**(24), 836–881 (2015)MathSciNetzbMATHGoogle Scholar - 4.Bialy, M., Lawford, M., Pantelic, V., Wassyng, A.: A methodology for the simplification of tabular designs in model-based development. In: Proceedings of the 3rd FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp. 47–53. IEEE Press, May 2015Google Scholar
- 5.Coecke, B., Kissinger, A.: Picturing Quantum Processes. Cambridge University Press, Cambridge (2017)CrossRefGoogle Scholar
- 6.Dragomir, I., Preoteasa, V., Tripakis, S.: Translating hierarchical block diagrams into composite predicate transformers. arXiv preprint arXiv:1510.04873 (2015)
- 7.Goncharov, S., Schröder, L.: Guarded traced categories. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 313–330. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89366-2_17CrossRefGoogle Scholar
- 8.Hasegawa, M.: Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi. In: de Groote, P., Roger Hindley, J. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 196–213. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-62688-3_37CrossRefzbMATHGoogle Scholar
- 9.Hofmann, M., Pierce, B., Wagner, D.: Symmetric lenses. In: ACM SIGPLAN Notices, vol. 46, no. 1, pp. 371–384 (2011)Google Scholar
- 10.Jin, Y., Parnas, D.L.: Defining the meaning of tabular mathematical expressions. Sci. Comput. Program.
**75**(11), 980–1000 (2010)CrossRefGoogle Scholar - 11.Joyal, A., Street, R., Verity, D.: Traced monoidal categories. In: Mathematical Proceedings of the Cambridge Philosophical Society, vol. 119, pp. 447–468. Cambridge University Press (1996)Google Scholar
- 12.Katis, P., Sabadini, N., Walters, R.F.C.: Span(Graph): A categorical algebra of transition systems. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 307–321. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0000479CrossRefGoogle Scholar
- 13.Lee, E.A., Varaiya, P.: Structure and Interpretation of Signals and Systems, 2nd edn. LeeVaraiya.org (2011)Google Scholar
- 14.Liebrenz, T., Herber, P., Glesner, S.: Deductive verification of hybrid control systems modeled in Simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 89–105. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02450-5_6CrossRefGoogle Scholar
- 15.Malherbe, O., Scott, P.J., Selinger, P.: Partially traced categories. J. Pure Appl. Algebra
**216**(12), 2563–2585 (2012)MathSciNetCrossRefGoogle Scholar - 16.Manamcheri, K., Mitra, S., Bak, S., Caccamo, M.: A step towards verification and synthesis from Simulink/Stateflow models. In: Proceedings of the 14th International Conference on Hybrid systems: Computation and Control, pp. 317–318. ACM (2011)Google Scholar
- 17.MathWorks: Simulink Design Verifier. https://www.mathworks.com/products/sldesignverifier.html (2018). Accessed 18 Nov 2018
- 18.McSCert: Simulink-to-Stateflow. https://www.mathworks.com/matlabcentral/fileexchange/70317-simulink-to-stateflow (2019). Accessed Feb 2019
- 19.Minopoli, S., Frehse, G.: SL2SX translator: From Simulink to SpaceEx models, April 2016. http://www-verimag.imag.fr/~minopoli/SL2SX.pdf
- 20.von Mohrenschildt, M.: Algebraic composition of function tables. Formal Aspects Comput.
**12**(1), 41–51 (2000)CrossRefGoogle Scholar - 21.Parnas, D.L.: Tabular representation of relations. McMaster University, Technical report, October 1992Google Scholar
- 22.Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke, B. (ed.) New Structures for Physics, vol. 813, pp. 289–355. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12821-9_4CrossRefzbMATHGoogle Scholar
- 23.Sfyrla, V., Tsiligiannis, G., Safaka, I., Bozga, M., Sifakis, J.: Compositional translation of Simulink models into synchronous BIP. In: 2010 International Symposium on Industrial Embedded Systems (SIES), pp. 217–220. IEEE (2010)Google Scholar
- 24.Singh, N.K., Lawford, M., Maibaum, T.S., Wassyng, A.: Stateflow to tabular expressions. In: Proceedings of the Sixth International Symposium on Information and Communication Technology (SolCT), p. 47. ACM (2015)Google Scholar
- 25.The MathWorks: MathWorks Automotive Advisory Board (MAAB): Control Algorithm Modeling Guidelines Using MATLAB, Simulink, and Stateflow, Version 3.0 (2012). www.mathworks.com/solutions/automotive/standards/maab.html
- 26.The MathWorks: Simulink user’s guide, September 2018. http://www.mathworks.com/help/releases/R2018b/pdf_doc/simulink/sl_using.pdf, http://www.mathworks.com/help/releases/R2015b/pdf_doc/simulink/sl_using.pdf, version R2018b. Accessed Feb 2019
- 27.Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embed. Comput. Syst. (TECS)
**4**(4), 779–818 (2005)CrossRefGoogle Scholar - 28.Wassyng, A., Janicki, R.: Tabular expressions in software engineering. In: Proceedings of 2003 International Conference on Software and System Engineering ICSSEA 2003, pp. 1–46 (2003)Google Scholar
- 29.Wynn-Williams, S.: SL2SF: Refactoring Simulink to Stateflow (2019), unpublished thesisGoogle Scholar
- 30.Zhan, N., Wang, S., Zhao, H.: Formal Verification of Simulink/Stateflow Diagrams, Springer (2017)Google Scholar
- 31.Zhou, C., Kumar, R.: Semantic translation of Simulink diagrams to input/output extended finite automata. Discrete Event Dyn. Syst.
**22**(2), 223–247 (2012)MathSciNetCrossRefGoogle Scholar

## Copyright information

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.