Information Technology Reference
In-Depth Information
We also relate our work to other methods for analyzing Simulink models.
Most tools that aim at formal analyses of Simulink models focus on a partic-
ular and usually relatively small fragment. In particular, models that contain
ANSI-C are often not considered [13,14,15]. Strichman and Ryabtsev [16] uses
an automated decision procedure to validate code generated by Simulink against
a set of verification conditions extracted from the model.
Another issue is the floating-point semantics of Simulink. Tools such as the
Simulink Design Verifier rely on approximations of floating point arithmetic by
means of infinite-precision rational numbers [17]. In contrast to that, we use a
bit-accurate representation of floating-point arithmetic, as presented in [18]. We
are therefore able to analyse the exact behaviour of the model rather than an
approximation. Furthermore, our bit-level technique enables the use of mutations
such as bit-flips in data values.
Outline.
Section 2 describes the transformation of Simulink diagrams into an
intermediate representation amenable to static analysis. This translation process
conclusively determines the semantics of the model. Section 3 discusses how fault
injection and mutations of the model and (bounded) model checking can be used
to generate test cases. For this purpose, we rely on a model checking technique
able to deal with floating-point arithmetic. We present a novel algorithm which
aims at identifying ecient test cases that cover more than one mutation, thus
reducing the size of the test suite and improving the performance of the test-
case generation process in Section 4. In Section 5, we discuss strategies to detect
mutations that do not have an observable impact on the model.
2 Simulink Models
The Simulink language is a graphical modeling language comprising block dia-
grams and an extensive set of block libraries. An example of a Simulink model
is presented in Figure 1. Due to the complexity of the language and the lack of
formal semantics, Simulink models are not directly amenable to automated anal-
ysis. We present a front-end to transform these models into intermediate ANSI-
C programs with well-defined semantics. This transformation is performed fully
automatically and allows us to separate the ambiguity issues in the Simulink
semantics from our test case generation process.
Each Simulink block is associated with a type. We define the meaning of blocks
of a particular type by means of C code, which is organized in a library. This
library can be independently refined or modified (e.g., to add a new block-type
definition) without the need to change the transformation process.
A
block-type
X
is defined with the following artifacts:
-
X in t
: a C struct that defines the input ports of
X
.
-
X out t
: a C struct that defines the output ports of
X
.
-
X props t
: a C struct that specifies the verification-relevant properties of
X
.
-
X semfun
: a C function that defines the semantics of
X
as a mapping from
input ports to output ports. Its declaration format is
X out t* X semfun(X props t *prop, X in t *in)
.
