Stateflow to Tabular Expressions

Conference Paper (PDF Available) · December 2015with 124 Reads 
How we measure 'reads'
A 'read' is counted each time someone views a publication summary (such as the title, abstract, and list of authors), clicks on a figure, or views or downloads the full-text. Learn more
DOI: 10.1145/2833258.2833285
Conference: the Sixth International Symposium
Cite this publication
Abstract
Stateflow is a visual tool that is used extensively in industry for designing the reactive behaviour of embedded systems. Stateflow relies on techniques like simulation to aid the user in finding flaws in the model. However, simulation is inadequate as a means of detecting inconsistencies and incompleteness in the model. Tabular Expressions (function tables) have been used successfully in software development for more than thirty years. Tabular expressions are also visual representations of functions, but include the important properties of completeness and disjointness. In other words, a tabular expression is well-formed only when the input domain is covered completely (completeness), and when there is no ambiguity in the behaviour described by the tabular expression (disjointness). The goal of our work is to use the completeness and disjointness properties of well-formed tabular expressions to aid us in establishing those properties in Stateflow models. From the Stateflow models, we generate a new kind of tabular expression that includes extended output options. We use the informal Stateflow semantics from MathWorks documentation as the basis for generating our tabular expressions. The generated tabular expressions are then used to guarantee completeness and disjointness. We provide a transformation algorithm that we plan to implement in a tool to automatically generate tabular expressions from Stateflow models.
Figures - uploaded by Mark Stephen Lawford
Author content
All content in this area was uploaded by Mark Stephen Lawford
Content may be subject to copyright.
Stateflow to Tabular Expressions
Neeraj Kumar Singh
IRIT-ENSEEIHT
University of Toulouse
Toulouse, France
nsingh@enseeiht.fr
Mark Lawford
McMaster Centre for Software
Certification
McMaster University
Hamilton, Ontario, Canada
lawford@mcmaster.ca
Thomas S. E. Maibaum
McMaster Centre for Software
Certification
McMaster University
Hamilton, Ontario, Canada
tom@maibaum.org
Alan Wassyng
McMaster Centre for Software
Certification
McMaster University
Hamilton, Ontario, Canada
wassyng@mcmaster.ca
ABSTRACT
Stateflow is a visual tool that is used extensively in industry for
designing the reactive behaviour of embedded systems. Stateflow
relies on techniques like simulation to aid the user in finding flaws
in the model. However, simulation is inadequate as a means of de-
tecting inconsistencies and incompleteness in the model. Tabular
Expressions (function tables) have been used successfully in soft-
ware development for more than thirty years. Tabular expressions
are also visual representations of functions, but include the impor-
tant properties of completeness and disjointness. In other words,
a tabular expression is well-formed only when the input domain
is covered completely (completeness), and when there is no am-
biguity in the behaviour described by the tabular expression (dis-
jointness). The goal of our work is to use the completeness and
disjointness properties of well-formed tabular expressions to aid
us in establishing those properties in Stateflow models. From the
Stateflow models, we generate a new kind of tabular expression
that includes extended output options. We use the informal State-
flow semantics from MathWorks documentation as the basis for
generating our tabular expressions. The generated tabular expres-
sions are then used to guarantee completeness and disjointness. We
provide a transformation algorithm that we plan to implement in a
tool to automatically generate tabular expressions from Stateflow
models.
CCS Concepts
Software and its engineering Consistency; Completeness;
Formal software verification; Software notations and tools; Re-
quirements analysis; Software design engineering;
Keywords
Stateflow; Tabular Expressions; completeness; disjointness
Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for profit or commercial advantage and that copies bear this notice and the full cita-
tion on the first page. Copyrights for components of this work owned by others than
ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or re-
publish, to post on servers or to redistribute to lists, requires prior specific permission
and/or a fee. Request permissions from permissions@acm.org.
SoICT 2015, December 03-04, 2015, Hue City, Viet Nam
c
2015 ACM. ISBN 978-1-4503-3843-1/15/12. . . $15.00
DOI: http://dx.doi.org/10.1145/2833258.2833285
1. INTRODUCTION
To hide complexity and to minimize the introduction of errors,
the software development process has changed dramatically over
the last few years. Software engineers and developers prefer to
use model-based development to design complex systems, where
graphical blocks and symbols can represent high level abstraction
of a system. Model-based development supports various tools based
on graphical blocks and symbols, which are used by industries for
design, simulation, and testing. Matlab is one of the tools that is
used worldwide by the automotive, medical and avionic industries
for developing their products.
Stateflow is a complex language with numerous features, but
does not have formal semantics. Its documentation [18] describes
informal semantics of the Stateflow execution based on the Matlab
simulation environment using various examples. Moreover, State-
flow does not support a formal verification tool for checking prop-
erties like consistency, completeness, and disjointness. The exist-
ing problems in Stateflow offer an opportunity to investigate tech-
niques that could provide such properties, as well as the capabil-
ity to verify a model’s consistency, taking into account Stateflow’s
informal semantics. In this paper, we propose the transformation
of Stateflow models into tabular expressions to address these prob-
lems. Tabular expressions have precise semantics [17, 16], and ver-
ification capabilities [8], and have been used for many years in in-
dustry [11, 32, 31]. We use the Stateflow informal narrative seman-
tics to capture precisely the order of execution of different compo-
nents of the Stateflow models. The generated tabular expressions of
a Stateflow model shows precise behavior of the system based on
tabular semantics by preserving the properties of disjointness and
completeness. This operational approach is able to express compli-
cated behaviours of a system in tabular expressions that are likely
to be lost in a state transition table. Moreover, the generated tab-
ular expressions include extended conditions, and behaviours that
are not explicitly clear in the original Stateflow models. These ex-
tended conditions and missing behaviours are identified during the
transformation process. The tabular expressions satisfy required
properties like consistency, completeness and disjointness and this
can be verified by existing tools [8]. The generated tabular expres-
sions contain detailed information that can be used further for an-
Partially supported by: The Ontario Research Fund, and the Na-
tional Science and Engineering Research Council of Canada.
312
alyzing the specific properties of a particular component of a very
large system. Moreover, the tabular expressions can be used by
software engineers and developers to understand desired system
behaviours more precisely.
The remainder of this paper is organized as follows. Section 2
presents related work. Section 3 introduces the characteristics of
Stateflow and tabular expressions. Section 4 shows the transforma-
tion process from Stateflow to tabular expressions. Experiments in
Section 5 demonstrate the applicability and usefulness of our ap-
proach. Section 6 discusses the paper, and Section 7 concludes the
paper along with potential future work.
2. RELATED WORK
Since the late 1950s, tables have been used for various purposes
like analyzing computer code, and developing requirements docu-
ments. In the 1960s, tables first appeared in the literature to show
their usability in software development [4, 20, 21]. All these tables
can be distinguished by their names and forms such as decision
tables, transition tables, etc.
Parnas and others introduced tabular expressions for developing
the requirements document for the A-7E aircraft [13, 6, 12, 22] in
work undertaken for the US Navy. Parnas was the most influential
person to apply tabular expressions in documenting software [27].
Later, tables were used by many others, including at Bell Labora-
tories, and the US Air Force. Starting in the late 1980s tabular no-
tations were applied by Ontario Hydro in developing the shutdown
systems for the Darlington Nuclear Plant [32, 31, 2, 25]. Formal se-
mantics of tabular expressions have been proposed by Parnas [23]
and other researchers [14, 15, 17, 16]. A slightly outdated survey
on tabular expressions is available in [16].
Stateflow is a graphical modelling language that shares many
features with Statecharts [10]. Stateflow semantics are completely
deterministic while Statecharts semantics can handle non-determinism.
For instance, the execution order among parallel states in State-
flow is sequential. Moreover, Stateflow has its own modelling fea-
tures such as defining that a condition action of a transition occurs
before its source state becomes inactive. Therefore, Statecharts
semantics are not applicable to Stateflow. However, several pa-
pers have reported work on formal verification of Stateflow mod-
els. Banphawatthanarak et al. [3] used the SMV model checker to
verify Stateflow models, in which they had not considered mod-
elling multiple hierarchy levels of states. Cavalcanti [5] proposed
verification of Stateflow models using the Circus specification lan-
guage. Scaife et al. [28] converted a subset of Stateflow into a
synchronous language, Lustre, in which inter level transitions were
not allowed. The operational semantics of Stateflow proposed by
Rushby et al. [9] have been used as a foundation for developing a
prototype tool for formal analysis of Stateflow designs.
A transition table is a tabular presentation of a Stateflow model,
that shows only the conditions and actions of transitions, and state
information. This table does not contain other information like
entry, exit and during actions. Due to this lack of information
in the transition table, it cannot be used for analyzing the con-
sistency, completeness and disjointness properties of a Stateflow
model. In order to analyze these properties, our approach is to
transform Stateflow models into tabular expressions or function ta-
bles using the narrative informal semantics of Stateflow that con-
tain detailed information about the actions and transitions. In this
way, entry, exit, during and condition actions also appear in their
proper order in the produced tabular expression. The tabular ex-
pression allows a careful inspection of the Stateflow model through
identifying missing conditions and desired behaviours by checking
completeness and disjointness.
3. PRELIMINARIES
3.1 Stateflow
In this section, we describe how the Stateflow language can be
used for designing complex behaviours of a system. Simulink is
a block diagram environment for modelling, simulating and ana-
lyzing a system, whereas Stateflow is an interactive tool that can
be used for modelling the behaviours of reactive systems. State-
flow models can be included in a Simulink model by placing them
in Stateflow blocks. The syntax of Stateflow is similar to State-
charts [10]. It supports the notions of hierarchy (states may con-
tain other states), concurrency (executes more than one state at the
same time), and communication (broadcast mechanism for commu-
nicating between concurrent components). It also includes com-
plicated features like inter level transitions, complex transitions
through junctions, and event broadcasting. These features allow
us to design complex systems effectively and concisely.
Fig. 1 depicts a simple Stateflow diagram, which contains all the
basic components of Stateflow. A Stateflow model consists of a
set of states connected by arcs called transitions. Each state has a
name and can be decomposed to model a hierarchical state diagram.
States can have different types of actions that can be executed in a
sequential order. These action types are entry,exit,during, and on
event_name.
There are two types of decomposition for a state: 1) OR-states
and 2) AND-states. In the Stateflow diagram, the OR-states are
indicated by a solid border, while AND-states are indicated by a
dashed border. Each hierarchy level of the Stateflow presents either
OR-states or AND-states decomposition (see Fig. 1). It should be
noted that, AND-states do not allow pure concurrency because the
Stateflow model runs on a single thread, therefore only one AND-
state executes at a time. Each AND-state is executed sequentially
according to the execution order, which can depend on the states’
geometric positions or manually assigned priorities. A Stateflow
model can have both data and event input/output ports that can be
defined as local as well as external.
A transition is an arc that connects two states, where one state
is source (state) and another is destination (state). A transition can
be characterized by a label that can consist of event triggers, condi-
tions, condition actions, and transition actions. The ‘?’ character is
the default empty label for transitions. A transition label can have
the following general format:
event [condition] condition_action/transition_action
Each part of the transition label is optional. The event specifies
an event that causes the transition to be taken, provided the con-
dition, if defined, is true. The absence of an event indicates that
the transition is taken upon the occurrence of any event. Multiple
events can be specified using the OR logical operator (see Fig. 1).
A condition is a boolean expression that indicates that the transi-
tion can be taken if the condition expression is true. A condition
action is enclosed in curly braces({}) and executes as soon as the
condition (guard) becomes true before the transition destination has
been determined to be valid. Absence of a condition expression is
implied by true, and the condition action is executed only if the
transition is true. The transition action is always executed after the
transition destination has been determined upon validation of the
provided condition. Each transition also has a priority of execu-
tion, which can be determined based on the geometric position and
hierarchy level.
Stateflow uses two different types of junctions named as connec-
tive and history junctions (see Fig. 1). The connective junctions
313
StateA
StateB
StateC StateD
StateF
StateG
StateE
StateH StateI
StateK
StateJ
H
StateP
StateQ
[t>10] {a=a+2;}/s=s+10;
Evt2
[t>5||a>10]
Evt2
Evt1|| Evt2
[t>5]
Evt1
Evt2
entry: a=0;
exit: a=10;
during: a=a+1;
entry: a=0;
exit: a=2;
exit: a=7;
during: s=s+1;
entry: a=0;
exit: a=4;
Default
Transition
Parallel (AND)
State
Exclusive (OR)
State
History
Junction
Transition
Connective
Junction
Transition ActionCondition ActionCondition
Event
State
Actions Transition Label
[t>10] {a=a+2;}/s=s+10;
Figure 1: Stateflow Example.
provide alternative transitions paths for a single transition or de-
sired system behaviour. They are often used to model an if-then-
else structure, a case structure or a for loop. The history junctions
record historical activity information of states or superstates. A his-
tory junction of a superstate stores the state or substate which was
active when the superstate was exited.
3.2 Tabular Expressions
In late 1970s, Parnas et al. [24, 25, 13] used tables to specify the
software system requirements for expressing complex behaviours
through organizing the relation between input and output variables.
These tables were used simply to describe the system requirements
unambiguously. Parnas formally defined ten different types of ta-
bles for different purposes using functions, relations, and predi-
cates [23]. Parnas also called these tables tabular expressions be-
cause the tables use mathematical expressions and recursive defi-
nitions. Some foundational works reported formal semantics [17],
table transformation, and composition of tables [30]. The formal
semantics of tables specify the precise meaning that helps to main-
tain the same level of understanding when tables are used by vari-
ous stakeholders. Similarly, table transformation can be used to get
a desired system behaviour under various system situations, and the
composition of tables can be used to integrate different tables to ob-
tain the final complex behaviour. These tables have been used by
several international projects like Ontario Hydro in the Darlington
Nuclear Plant [7], and the US Naval Research Laboratory [11], etc.
Tabular expressions [26, 27] are not only effective visually, and
an effective and simple approach to documenting the system re-
quirements by describing conditions and relations between input
and output variables, they also facilitate preserving essential prop-
erties like completeness and disjointness. In our work, for trans-
forming Stateflow models into tabular expressions, we use horizon-
tal condition tables (HCT) shown in Fig. 2. The HCT table contains
a group of columns for input conditions and a group of columns for
output results. However, the input column may be sub-divided to
specify multiple sub-conditions. The tabular structure highlights
the structure of predicates, and adjoining cells are considered to be
ANDed (see Fig. 2) that can be interpreted in the tabular structure
as a list of "if-then-else" predicates.
Condition 1
Condition f_name
Sub Condition 1
Sub Condition 2
.... .... ....
Condition n
Result 1
Result 2
....
Result n
Figure 2: Horizontal Condition Table or Function Table.
4. RULES FOR TRANSFORMING STATE-
FLOW INTO TABLES
Stateflow models can be designed using graphical components
(states and transitions) as well as state transition tables. Both the
graphical representation and transition table of a Stateflow model
often contains inconsistencies and may be incomplete. In this sec-
tion, we describe the general rules for transforming Stateflow mod-
els into tabular expressions according to the narrative executional
semantics of Stateflow, in order to analyze complex behaviours, and
to guarantee essential properties like consistency, completeness and
disjointness through discovering missing information. This miss-
ing information is often considered as not to be part of the system
design. In this paper, we consider simple Stateflow models that can
allow only exclusive (OR) states without hierarchy. But the simple
314
Condition
Actions
Entry
Actions
Exit
Actions
Transition
Actions
During
Actions
Condition
Event
Source
State
Destination
State
..... ..... ..... ..... ..... ..... ..... ..... .....
du_action1en_action
du_actionn
...
cnd_action1
cnd_actionp
...
ex_action1
ex_actionq
...
tran_action
tran_action
... 1
ren_actions
... 1
Figure 3: Table Architecture for Stateflow.
Stateflow models do allow entry,during,exit,condition and transi-
tion actions. In the following sections, we describe an architecture
of the table and a set of rules for transforming Stateflow models
into tabular expressions.
4.1 Tabular Expression Architecture for State-
flow
To preserve the narrative semantics of Stateflow, we use output
columns of HCT in a specific order. Fig. 3 presents an architecture
of the tabular expressions, which contains the elements of State-
flow model. In the Fig. 3, first three columns contain Source State,
Event, and Condition of a transition. The cells of these columns
can be further split into two or more cells as per the requirement
during the transformation process to cover the possible scenarios
for complex properties. For example, the conditions of a transition
do not contain negation of the given conditions that must be iden-
tified during the generation of tabular expressions. The rest of the
columns of Fig. 3 contain ordered During Actions,Condition Ac-
tions,Exit Actions,Transition Actions,Destination State and Entry
Actions. Let nbe the number of user defined program variables
appearing in a Stateflow block. All of the Actions columns may be
split into many sub-columns to record the possible actions on these
nvariables. In the Stateflow, a variable can be used many places.
For instance, a variable can be in both Exit Action and Transition
Action, and these actions matter on the execution order. To handle
the multiple times appearance of the same variable, we apply spe-
cialization to distinguish all the Stateflow variables. For example,
we use some extra tags on each variable name as per the type of
action, such as, for Exit Action variable name can be ex_var, where
exit belongs to the Exit Action and var is a variable name. We also
use some fixed keywords like NONE, NC, and CALL that can be
used to fill the cells of the table. The meanings of these keywords
are as follows: NONE when an action is not given, NC for No
Change (a value is not modified after execution), and CALL for
function or events calling in the actions.
It should be noted that we have considered During Action be-
fore the rest of the action columns and destination state, because
the during action(s) of the source state is only allowed when all the
transitions are invalid from the source state to all the possible desti-
nation states. In this case, we need to fill only during action(s) and
the destination state with the same value as the source state, and the
rest of the columns do not change.
4.2 Transformation Rules
This section provides a set of rules for transforming the State-
flow models into tabular expressions. We have identified these rules
through our understanding of the Stateflow executional semantics,
and the rules are then applied to transform the Stateflow models.
Our current rules deal with only simple Stateflow models in which
parallel and hierarchy levels of modelling are not included. How-
ever, this is our first step in applying tabular expressions to analyze
Stateflow models through transformation. In the future, we will
provide transformation rules for other complex Stateflow models,
including parallel and hierarchical models. These transformation
rules will extend the simple Stateflow rules to cover all the required
functional behaviors for checking the properties of disjointness and
completeness. In fact, the simple Stateflow covers all the essen-
tial information that can be required by the parallel and hierarchy
Stateflow models. A set of rules can be applied iteratively to cover
all the states and transitions for transforming the simple Stateflow
models into the specific table format we have defined (see Fig. 3).
The current rules are given in a narrative style as follows:
1. Default / Normal Transition: Identify a default transition
or normal transition.
2. Source State: The next step is to identify a source state of
the identified transition and add it into the source state col-
umn of the table (in case of default transitions set source state
to START).
3. Event: In this step, we analyze the label of an identified out-
going transition from the source state. If this transition con-
tains one or more events then we add them into the event
column of the table, otherwise we place TRUE into the event
column of the table. (The event element is optional so it can
be absent sometimes).
4. Condition: Identify the given condition(s) of the transition
and add it into the condition column of the table (if condi-
tion(s) are absent then set the condition to TRUE).
5. Condition Action: The next step is to identify the given con-
dition action(s) of the identified transition, and add it into the
condition action column of the table (if the condition action
is absent then set the condition action to NC). If more than
one condition action is identified, then with the variable’s
name use specialization and all these new specialized vari-
ables will be added into multiple sub-columns of the action
column of the table. If the given condition action is an event
or predefined function then use CALL function or event.
6. Exit Action: The next step is to identify the exit action(s)
of the source state, add it into the column of exit action of
the table. If more than one exit actions is identified then with
the variable’s name use specialization with exit action(s) to
fill other sub-columns of the exit action column. If the given
exit action is an event or predefined function then use CALL
function or event.
7. Transition Action: This step is used to identify the tran-
sition action(s) and add it into the transition action column
of the table. If more than one transition action is identified,
then with the variable’s name use specialization with transi-
tion action(s) to fill other sub-columns of the transition ac-
tion. If the given transition action is an event or predefined
function then use CALL function or event.
8. During Action: The next step is to identify the during ac-
tion(s) of the source state, and add it into the during action
column of the table. During actions are included only when
there are no valid transitions available, causing the state to
remain active (i.e. source state = destination state). If more
than one during action is identified, then with the variable’s
name use specialization with during action(s) to fill other
sub-columns of the during action. If the given during action
315
Event Condition Condition
Action
Exit
Action
Default
Transition
True
False
True
True Transition
Action
Destination
State
Entry
Action
False
During
Action
Source
State
Default
Transition
Default
Transition
False
True
False
Figure 4: Building Tables from Stateflow : Abstract Flowchart.
is an event or predefined function then use CALL function or
event.
9. Destination State: In this step, we identify the destination
or target state and add it into the destination state column of
the table. For any during action(s), the destination state must
be the same as the source state.
10. Entry Action: Finally, we identify the entry action(s) in the
target or destination state and add it into the entry action col-
umn of the table. If more than one entry action is identified,
then with the variable’s name use specialization to fill other
sub-columns of the entry action. If the given entry action is
an event or predefined function then use CALL function or
event.
11. Completeness of Events and Conditions: Corresponding
to the split cells in the columns of event and condition, make
respective entries in the entire row through splitting the rest
of the cells in each column. For example, for input domain
completeness related to an event, add the negation of the
given event(s) in the same column by splitting the cell into
two or more cells (if an event does not exist then this step is
not required); and for completeness of the input domain re-
lated to conditions, add the negation of the condition(s) in the
same column by splitting the cell into two or more cells. It is
important that the identified condition(s) and its negation be
added into the table for the identified event and its negation
as well. It should be noted that in the case of a during action
all the cells will use NC as a cell value except a destination
state cell entry, which will be the same as the source state.
12. Goto Step 1.
The above rules apply iteratively to transform the Stateflow mod-
els into tabular expressions. The textual description of the rules
may appear complex, but the transformation process is actually
quite straightforward. To better understand this process, we have
included an abstract view of the transformation process using a
flowchart (see Fig. 4).
5. CASE STUDY
In this section, we apply the transformation rules for generating
the tabular expressions from Stateflow models. We have applied
this transformation process to several case studies and industrial ex-
amples, in which a system is developed without using hierarchical
and parallel components of Stateflow. However, we would like to
share our experience with a real-time case study related to a robotic
system, which is taken from [1]. It is a small case study that is de-
veloped by researchers for the Field Robot Event 2007. The given
stateflow model is used for designing the behaviour of a robotic
system. Fig. 5 presents a basic exclusive (OR) Stateflow chart of
the robotic system. We applied our transformation process to ob-
tain the tabular expressions from the selected Stateflow models of
the robotic system that captures all the possible activities including
different types of actions, transitions and state information. Fig. 6
shows the generated tabular expression. In Fig. 5, a default transi-
tion is identified that is used initially to start the process for gener-
ating the tabular expressions (see Fig. 6). In Fig. 6, the first row of
the column Source State contains State =ST AR T to present the
default transition of the robotic stateflow. In the case of a normal
transition the column Source State contains the name of the source
state in place of START. For example, the next row of the same
column contains State == M anualDrive. The next column
(Event) of the table contains T RU E that shows there is no ex-
plicit event associated with the default transition. The default tran-
sition of the robotic stateflow has three transitions connected by a
junction. These three transitions have transition conditions that are
given in the column Condition of the table in three separate rows.
For example, stateReq == 1 is the condition for the first transi-
tion, stateReq == 2 OR stateReq == 3 OR stateReq == 5
OR stateReq == 12 is the condition for the second transition,
and stateReq == 4 is the condition for the third transition. The
default transition does not have a source state, therefore the During
Actions column of the table contains NC. Similarly, the transitions
do not have condition actions and exit actions so that the next two
columns, Condition Actions and Exit Actions are set to NC. The
next column, Transition Action, contains a list of actions that are
placed in three separate rows, one for each transition. For example,
drivingDirOut = 1; turnCounter = 1; is a list of sequential
actions for the first transition, drivingDirOut = 1; turnCounter = 1;
state = stateReq; is a set of sequential actions for the second tran-
sition and drivingDirOut = 1; turnCounter = 1; state = 4;
is a list of sequential actions for the third transition. To distin-
guish these variables drivingDirOut,turnCounter and state from
other actions (e.g. exit, during), we can use specialization, such
as tran_drivingDirOut,tran_turnCounter and tran_state, in which
tran’ indicates for transition action (see Fig. 3). The next column,
Destination State, is used to set a destination state corresponding
to the selected transition. In the example, three destination states
ManualDrive,drivingRow and Turning are set in the Destination
State column of the table for each transition. Finally, the last col-
umn, Entry Actions, is used to place a list of entry actions of the
destination state in the table. In our running example, there is no
entry action in any of the three destination states ManualDrive,
drivingRow and T urning, therefore we enter NC in each row of
the transitions. In order to satisfy completeness properties in the
table, we need to add an extra row with the negation of the given
transitions conditions. In this case, we make the Destination State
the same as the source state, the During Actions column contains a
list of during actions, and the rest of the columns of the table are
set to NC. In our example, we use negation of all the conditions of
the given transitions as ((stateReq == 1) OR (stateReq == 2
OR stateReq == 3 OR stateReq == 5 OR stateReq == 12)
OR (stateReq == 4)) and the rest of the columns are set to NC
because there is no during action in the source state. The Desti-
nation State column must also be the same as the source state. In
a similar way, we applied all the transformation rules to cover all
remaining states and transitions to produce the tabular expression
in (see Fig. 6). The generated table contains much more significant
information than the transition table. In the generated table, the
condition column has some highlighted boldface conditions. These
conditions do not exist in the Stateflow model. These conditions
316
Figure 5: Stateflow models of a Robotic System [1].
are discovered during the transformation process used to generate
the tabular expression, since we have to ensure that the tabular ex-
pression is disjoint and complete. It should be noted that the asso-
ciated row for each condition is produced in the table according to
‘discovered’ conditions. We have used this transformation process
on several other Stateflow models to generate tabular expressions.
We have observed through this experiment that most of the time
a Stateflow model does not satisfy disjointness and completeness
properties, which are essential for developing critical systems. Our
experiment results have provided enough evidence to assert that
often a Stateflow model does not satisfy essential properties like
completeness and disjointness, and this is not safe for developing
a safe and dependable system. Checking properties like complete-
ness, disjointness and consistency are not easy without tool support.
Therefore, we have used our previously developed tool [8] to check
completeness, disjointness and consistency.
6. DISCUSSION
Simulink is a visual notation that is used by many industries, in-
cluding automotive, avionics and medical, to design complex sys-
tems. Stateflow is a graphical component of Simulink to model the
reactive behaviour of a system. Simulation techniques are a com-
mon approach for checking the validity of, and tracing errors in
Stateflow models. Simulink Design Verifier [19] is an extension of
the MathWorks Matlab / Simulink tool set that uses formal methods
to identify design errors in models. These errors include dead logic,
integer overflow, division by zero, and violations of design prop-
erties and assertions. Moreover, Simulink Design Verifier is also
used to analyze Simulink models to check the correctness of given
properties. These properties are specified directly in Simulink and
Stateflow in the form of assertions. Simulink Design Verifier uses a
prover plug-in to prove the given properties by searching for possi-
ble values for Simulink and Stateflow functions. It cannot be used
to check unsupported elements that may cause incomplete anal-
ysis or that will be stubbed out during analysis. According to [9],
Simulink does not support an interpretation of concurrency in terms
of a nondeterministic interleaving of concurrent events. Hence, the
Simulink Design Verifier does not check safety properties related
to concurrency, like race conditions. Moreoever, Simulink Design
Verifier does not support checks for disjointness and completeness
in the system requirements. In fact, simulation, like testing, cannot
guarantee the safe and reliable behaviour of a system that is devel-
oped with the help of Stateflow. It is obviously useful to be able
to complement these approaches by mathematical analysis. Unfor-
tunately, we do not have formal semantics for Stateflow. It should
be noted that the operational semantics presented in [9] are not suf-
ficient to check disjointness and completeness properties. We do
have some narrative semantics provided by MathWorks [18]. The
narrative semantics are not easy to comprehend and apply, and this
is why practitioners have relied on simulation to understand the
meaning of Stateflow models. As we have demonstrated, Stateflow
models often lack of disjointness and completeness properties, and
it is easy to miss subtle behaviours in the graphical presentation of
a complex and large Stateflow model, because the developer has
to keep in mind the complex semantics governing the ordering of
actions. Regulators and certification bodies are striving for reli-
able techniques [29] to guarantee the safe behaviour of systems
that are developed using Stateflow. In this context, we have pro-
posed the idea of generating a tabular expression from a Stateflow
model to address the described issues. In this paper, we have pre-
sented a list of translation rules to generate a table that contains
more significant information than the Stateflow model from which
it was derived. This approach has three primary benefits: firstly,
we have spent the time and effort necessary to understand the in-
formal semantics provided by MathWorks [18], and will generate a
consistent interpretation of Stateflow models, compared with what
happens now when different groups have slightly different inter-
317
Condition
Event
Source
State
State == START
State = ManualDrive
State == drivingRow
State == endOfRow
State == sequencEnded
State == Turning
TRUE
stateReq == 1
stateReq == 2 OR
stateReq == 3 OR
stateReq == 5 OR
stateReq == 12
stateReq == 4
¬ ((stateReq == 1) OR
(stateReq == 2 OR
stateReq == 3 OR
stateReq == 5 OR
stateReq == 12 ) OR
(stateReq == 4))
NC
NC
NC
NONE NONE
TRUE
rowEnd == 1 OR
rowEnd == 2
¬(rowEnd == 1 OR
rowEnd == 2)
rowEnd == 0
rowEnd == 2
(stateReq == 3 OR
stateReq == 5)
¬ ((rowEnd == 0) OR
(rowEnd == 2 ))
TRUE
NONE NONE
TRUE
¬(stateReq == 5)
(stateReq == 5)
NC
NC
NC
NC
NC
NC
During
Actions
state=1;
state_internal=6;
controlOut=controlIn;
drivingDirOut=drivingDirIn;
CALL weedKilling();
CALL calcAvgDir();
state_internal=1;
CALL slowDown();
CALL calcAvgDir();
state_internal=2;
playSound=0;
controlOut=0;
state_internal=5;
Condition
Actions
Exit
Actions
Transition
Actions
Destination
State
Entry
Actions
NC
drivingDirOut=1;
turnCounter=1;
state=stateReq;
tempDist=
traveledDist
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
ManualDrive
drivingRow
Turning
State
State
endOfRow
State
drivingRow
sequenceEnded
Turning
State
State
sequenceEnded
hitRow
drivingDirOut=1;
turnCounter=1;
state=4;
drivingDirOut=1;
turnCounter=1; NC
NC
NC
NC
NC
NC
NC
NC
controlOut=0;
NC
NC
NC
controlOut=0;
endRapu=0;
avgDirN=0;
State == hitRow TRUE
¬(rowEnd == 2)
(rowEnd == 2) NC
NC
sequenceEnded
State
endRapu == 1
¬(endRapu == 1) CALL driveForwards();
turnCounter=
turnCounter+1;
nextRow=
turnArray[turnCounter];
drivingRow
controlOut=0;
NC
NC
NC NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
turnCounter=
turnCounter+1;
nextRow=
turnArray[turnCounter];
¬(stateReq == 3 OR
stateReq == 5)
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
NC
Figure 6: Generated tabular expressions of the Robotic System.
pretations of the informal semantics; secondly, the generated table
is very easy to comprehend and it contains self explanatory details
for system behaviour according to those informal semantics; and
thirdly, the generated table satisfies disjointness and completeness
properties. Thus, the generated tabular expression of a complex
and large Stateflow model shows system behaviour equivalent to
the Stateflow narrative semantics in a way that makes the complete
behaviour more readily understandable, and also satisfies disjoint-
ness and completeness properties on the input predicates. This ap-
proach can assist in the construction, clarification, and validation of
Stateflow models. It should be noted that during the generation of
tabular expression from the robotic Stateflow model, we have found
some unwanted or incomplete transition conditions, which may al-
low some undesired behaviours. In fact, these unwanted or incom-
plete conditions prevent the generated table from being complete
and disjoint. We have rewritten the transition conditions without
changing the original behaviour to achieve disjointness and com-
pleteness properties in our generated table. However, we are still
investigating such types of unwanted or incomplete design patterns
in other Stateflow models that can be removed with the help of our
proposed solution. Moreover, this approach has the potential to
help regulators and certification bodies asses the quality of systems
that are developed using Stateflow models.
7. CONCLUSION AND FUTURE WORK
The use of model based development is growing extremely rapidly,
and some of the associated tools hide important system complex-
ities. These tools may provide a very rich set of graphical block
diagrams or symbols for developing complex behaviours. Mat-
lab/Simulink is one of the tools that has been adopted by many
industries for developing complex products. Stateflow is a com-
ponent of Simulink, and its narrative executional semantics cannot
guarantee essential properties like completeness, disjointness and
consistency, and often leads to the introduction of design flaws dur-
ing system modelling.
In this paper, we proposed the idea of transforming Stateflow
models into tabular expressions, in order to analyze the complete-
ness, disjointness, and consistency of Stateflow models. We are
interested primarily in guaranteeing completeness and disjointness
properties of Stateflow. Our proposed approach for transforming
Stateflow models into tabular expressions can identify missing be-
haviour to make it complete, and to identifying overlapping be-
haviours, so that we can make it disjoint. Moreover, we are still
developing semantics of the table to cope with the action columns
318
(not covered by tabular expression semantics). At the present time,
we have transformed the Stateflow models into tabular expressions
manually, but we have used a formal tool for checking consistency,
completeness and disjointness properties.The given transformation
rules in this paper are applicable for generating tabular expressions
from simple Stateflow models in a restrictive way. Our current
transformation rules do not cope with hierarchy and parallel state
models, including connective and history junctions. However, the
transformation rules do preserve the simulation semantics of the
Stateflow behaviour in the defined architecture of the table, and are
an indication of what we should be able to achieve once we have
built a more complete set of rules. The proposed transformation
rules are well suited to automatic processing.
In future work, we plan to investigate rules for transforming hier-
archical level Stateflow models and parallel Stateflow models into
tabular expressions, and then develop a tool to automate the trans-
formation process. Another possible direction to extend this work
is to consider the timing behaviour in Stateflow models.
8. REFERENCES
[1] http://autsys.aalto.fi/en/fieldrobot2007.
[2] G. Archinoff, R. Hohendorf, A. Wassyng, B. Quigley, and
M. Borsch. Verification of the shutdown system software at
the darlington nuclear generating station. In International
Conference on Control and Instrumentation in Nuclear
Installations, Glasgow, UK, 1990.
[3] C. Banphawatthanarak, B. Krogh, and K. Butts. Symbolic
verification of executable control specifications. In Computer
Aided Control System Design, 1999. Proceedings of the 1999
IEEE International Symposium on, pages 581–586, 1999.
[4] H. N. Cantrell, J. King, and F. E. H. King. Logic-structure
tables. Commun. ACM, 4(6):272–275, June 1961.
[5] A. Cavalcanti. Stateflow diagrams in circus. Electron. Notes
Theor. Comput. Sci., 240:23–41, July 2009.
[6] P. Clements. Function Specifications for the A-7E Function
Driver Module. NRL Memorandum Report. Defense
Technical Information Center, 1981.
[7] D. Craigen, S. Gerhart, and T. Ralston. Case study:
Darlington nuclear generating station. IEEE Softw.,
11(1):30–39, 28, Jan. 1994.
[8] C. Eles and M. Lawford. A tabular expression toolbox for
matlab/simulink. In NASA Formal Methods, pages 494–499,
2011.
[9] G. Hamon and J. Rushby. An operational semantics for
stateflow. Int. J. Softw. Tools Technol. Transf., 9(5):447–456,
Oct. 2007.
[10] D. Harel. Statecharts: A visual formalism for complex
systems. Sci. Comput. Program., 8(3):231–274, June 1987.
[11] C. Heitmeyer, J. Kirby, B. Labaw, and R. Bharadwaj. Scr: A
toolset for specifying and analyzing software requirements.
In A. Hu and M. Vardi, editors, Computer Aided Verification,
volume 1427 of Lecture Notes in Computer Science, pages
526–531. Springer Berlin Heidelberg, 1998.
[12] K. Heninger. Specifying software requirements for complex
systems: New techniques and their application. Software
Engineering, IEEE Transactions on, SE-6(1):2–13, 1980.
[13] K. Heninger, J. Kallander, and S. J. E. Parnas D. L. Software
Requirements for the A-7E Aircraft. NRL Memorandum
Report 3876. Naval Research Laboratory, 1978.
[14] R. Janicki. Towards a formal semantics of parnas tables. In
Proceedings of the 17th International Conference on
Software Engineering, ICSE ’95, pages 231–240, New York,
NY, USA, 1995. ACM.
[15] R. Janicki, D. Parnas, and J. Zucker. Tabular representations
in relational documents. In C. Brink, W. Kahl, and
G. Schmidt, editors, Relational Methods in Computer
Science, Advances in Computing Sciences, pages 184–196.
Springer Vienna, 1997.
[16] R. Janicki and A. Wassyng. Tabular expressions and their
relational semantics. Fundam. Inform., 67(4):343–370, 2005.
[17] Y. Jin and D. L. Parnas. Defining the meaning of tabular
mathematical expressions. Science of Computer
Programming, 75(11):980 – 1000, 2010. Special Section on
the Programming Languages Track at the 23rd {ACM}
Symposium on Applied Computing 08.
[18] Mathworks. Stateflow and Stateflow Coder, User’s Guide,
2003.
[19] Mathworks. Simulink Design Verifier, User’s Guide, 2011.
[20] M. Montalbano. Tables, flow charts, and program logic. IBM
Syst. J., 1(1):51–63, Sept. 1962.
[21] R. C. Nickerson. An engineering application of
logic-structure tables. Commun. ACM, 4(11):516–520, Nov.
1961.
[22] D. L. Parnas. A generalized control structure and its formal
definition. Commun. ACM, 26(8):572–581, Aug. 1983.
[23] D. L. Parnas. Tabular representation of relations. Technical
report, McMaster University, 1992.
[24] D. L. Parnas. Inspection of safety-critical software using
program-function tables. In IFIP Congress (3), pages
270–277, 1994.
[25] D. L. Parnas, G. J. K. Asmis, and J. Madey. Assessment of
Safety-Critical software in nuclear power plants. Nuclear
Safety, 32(2):189–198, June 1991.
[26] D. L. Parnas and J. Madey. Functional documents for
computer systems. Sci. Comput. Program., 25(1):41–61, Oct.
1995.
[27] D. L. Parnas, J. Madey, and M. Iglewski. Precise
documentation of well-structured programs. IEEE Trans.
Softw. Eng., 20(12):948–976, Dec. 1994.
[28] N. Scaife, C. Sofronis, P. Caspi, S. Tripakis, and
F. Maraninchi. Defining and translating a "safe" subset of
simulink/stateflow into lustre. In Proceedings of the 4th ACM
International Conference on Embedded Software, EMSOFT
’04, pages 259–268, New York, NY, USA, 2004. ACM.
[29] N. K. Singh. Using Event-B for Critical Device Software
Systems. Springer-Verlag GmbH, 2013.
[30] M. von Mohrenschildt. Algebraic composition of function
tables. Formal Aspects of Computing, 12(1):41–51, 2000.
[31] A. Wassyng and M. Lawford. Lessons learned from a
successful implementation of formal methods in an industrial
project. In FME, pages 133–153, 2003.
[32] A. Wassyng, M. Lawford, and T. S. E. Maibaum. Software
certification experience in the canadian nuclear industry:
lessons for the future. In EMSOFT, pages 219–226, 2011.
319
  • Chapter
    Full-text available
    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.
  • Chapter
    Formal methods based system development is considered as a promising approach to develop the safe critical systems. This chapter discusses the standard safety life-cycle, traditional safety analysis techniques, traditional system engineering approach, standard design methodologies and safety standards that are used for developing the critical systems. Furthermore, we have given a list of successful industrial case studies based on formal techniques. Moreover, we discuss the role of medical device regulations. Finally, this chapter shows the usability of formal techniques for developing the critical systems and to motivate for developing a new methodology, and associated techniques and tool in the context of medical device development, which are covered in the remaining chapters.
  • Chapter
    The most important step in the software-development life-cycle is the code implementation. This chapter presents a design architecture of an automatic code generation tool, which can generate code into several programming languages (C, C++, Java and C#). This tool is a collection of plug-ins, which are used for translating the Event-B formal specifications into multiple programming languages. The translation tool is rigorously developed with safety properties preservation. This is an essential tool, which supports code implementation phase of our proposed development life-cycle methodology for developing the critical systems.
  • Article
    We present a broad extension of the conventional formalism of state machines and state diagrams, that is relevant to the specification and design of complex discrete-event systems, such as multi-computer real-time systems, communication protocols and digital control units. Our diagrams, which we call statecharts, extend conventional state-transition diagrams with essentially three olements, dealing, respectively, with the notions of hierarchy, concurrency and communication. These transform the language of state diagrams into a highly structured' and economical description language. Statecharts are thus compact and expressive--small diagrams can express complex behavior--as well as compositional and modular. When coupled with the capabilities of computerized graphics, statecharts enable viewing the description at different levels of detail, and make even very large specifications manageable and comprehensible. In fact, we intend to demonstrate here that statecharts counter many of the objections raised against conventional state diagrams, and thus appear to render specification by diagrams an attractive and plausible approach. Statecharts can be used either as a stand-alone behavioral description or as part of a more general design methodology that deals also with the system's other aspects, such as functional decomposition and data-flow specification. We also discuss some practical experience that was gained over the last three years in applying the statechart formalism to the specification of a particularly complex system.
  • Article
    Full-text available
    This article outlines an approach in the design, documentation, and evaluation of computer systems. This allows the use of software in many safety-critical applications because it enables the systematic comparison of the program behavior with the engineering specifications of the computer system. Many of the ideas in this article have been used by the Atomic Energy Control Board of Canada in its safety assessment of the software for the shutdown systems of the Darlington Station. The four main elements of this approach follow: (1) Formal Documentation of Software Requirements: Most of the details of a complex environment can be ignored by system implementers and reviewers if they are given a complete and precise statement of the behavioral requirements for the computer system. We describe five mathematical relations that specify the requirements for the software in a computerized control system. (2) Design and Documentation of the Module Structure: Complexity caused by interactions between separately written components can be reduced by applying Data Abstraction, Abstract Data Types, and Object-Oriented Programming if the interfaces are precisely and completely documented. (3) Program Function Documentation: Software executions are lengthy sequences of state changes described by algorithms. The effects of these executive sequences can be precisely specified documented with tabular presentations of the program functions. Also, large programs can be decomposed and presented at a collection of well-documented smaller programs. (4) Tripod Approach to Assessment: There are three basic approaches to the assessment of complex software products: (i) testing, (ii) systematic inspection, and (iii) certification of people and processes. Assessment of a complex system cannot depend on any one of these alone. The approach used on the Darlington shutdown software, which included systematic inspection as well as planned and statistically designed random testing, is outlined.
  • Article
    As part of the experimental redesign of the flight software for the Navy's A-7E aircraft, software modules were designed to encapsulate the characteristics of the behavioral requirements of the system. The purpose of these Function Driver modules is to allow the remainder of the software to remain unchanged when the required system behavior is modified without associated hardware changes. This document specifies the behavior of the system without regard to specific hardware devices. This report contains an explanation of the standard organization of each functional description, a descrip-tion of the review procedure, specifications for all of the functional aspects of the A-7 software, and a set of indices and cross-references to help integrate this module with the rest of the system.
  • Chapter
    A controversial issue in the formal methods community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method and its support tools. This paper describes the SCR (Software Cost Reduction) tools, part of a practical formal method—a. method with a solid mathematical foundation that software developers can apply without theorem proving skills, knowledge of temporal and higher order logics, or consultation with formal methods experts. The SCR method provides a tabular notation for specifying requirements and a set of light-weight tools that detect several classes of errors automatically. The method also provides support for more heavy-duty tools, such as a model checker. To make model checking feasible, users can automatically apply one or more abstraction methods.
  • Article
    Mathematical expressions in tabular form (also called “tabular expressions” or “tables”) have been shown to be useful for documenting and analysing software systems. They are usually easier to read than conventional mathematical expressions but are no less precise. They can be used wherever mathematical expressions are used. To avoid misunderstandings, and to support users with trustworthy tools, the meaning of these expressions must be fully defined.This paper presents a new method for defining the meaning of tabular expressions. Each definition of an expression type names the expression’s constituents, and provides a restriction schema and one or more evaluation schemas. The restriction schema defines the class of well-formed expressions of the type. An evaluation schema maps a well-formed tabular expression of the type to a mathematical expression of a previously defined type. Since the meaning of conventional mathematical expressions is well known, describing an equivalent expression fully defines the meaning of a tabular expression.In this approach, indexation is used to decouple the appearance of a tabular expression from its semantics. A tabular expression is an indexed set of grids; a grid is an indexed set of expressions. The expressions in a grid can be either conventional expressions or tabular expressions of a previously defined type.Defining the meaning of a tabular expression in this way facilitates the building of tools that faithfully implement the semantics. The decoupling of syntax and semantics by means of indices overcomes some limitations of older approaches.The method presented in the paper is illustrated by defining several previously known types of tabular expressions and some new ones. The use of the new model to build a suite of tools for the input, presentation, validation, evaluation, simplification, conversion and composition of tabular expressions is discussed.
  • Conference Paper
    In [8, 11, 12] Parnas at al. advocate the use of relational model for documenting the intended behaviour of programs. In this method, tabular expressions (or tables) are used to improve readability so that formal documentation can replace conventional documentation. Parnas [9] describes several classes of tables and provides their formal syntax and semantics. In this paper, an alternative, more general and more homogeneous semantics is proposed.
  • Conference Paper
    Full-text available
    Tabular expressions have been successfully used in developing safety critical systems, however insufficient tool support has hampered their wider adoption. To address this shortfall we have developed the Tabular Expression Toolbox for Matlab/Simulink. An intuitive user interface allows users to easily create, modify and check the completeness and disjointness of tabular expressions using the ATP PVS or SMT solver CVC3. The tabular expressions are translated to m-functions allowing their seamless use with Matlab’s simulation and code generation.