Mapping UML to Labeled Transition Systems for Test-Case Generation - Formal Methods for Components and Objects - page 215

Any satisfying assignment to this formula represents two executions of M and
M that yield a different output sequence. The models are equivalent (up to k
steps) if Formula (1) is unsatisfiable.
Checking software equivalence is more complicated, since the two programs
rarely perform input/output in lockstep. Algorithmic details of equivalence check-
ing using BMC are covered in [3]. An approach based on predicate abstraction [20]
is presented in [21].

3.4 Floating-Point Arithmetic

Simulink models make heavy use of floating-point arithmetic (FPA). Although
reasoning about FPA is an active field of research, existing methods are primar-
ily tailored to interactive proof assistants (e.g., [22,23]) or abstract floating-point
number to intervals of the reals (e.g., [24,25]). The methods of the first kind are
unsuitable for automated tools, while the latter ones are not able to construct
models for satisfiable formulae and therefore cannot be used for test-case gener-
ation. Currently, there are only few model checkers that handle FPA accurately.
In our model checker Cbmc, we use the mixed abstraction framework de-
scribed in [18]. By using both over- and under-approximations simultaneously,
combined with a novel abstraction refinement approach, we are able to achieve
both accurate reasoning and a significantly better performance than ordinary
bit-blasting approaches [26].
Previous work on test case generation for Simulink programs, for instance in
the Simulink Design Verifier [17], employs approximations of floating-point arith-
metic by means of infinite-precision rational numbers. While this allows ecient
reasoning in the case of models only containing linear arithmetic, rationals do
not faithfully reflect the actual behavior of Simulink programs: in equivalence
checking, it can happen that Simulink models are erroneously reported as equiv-
alent (although they are not with FPA semantics), or that equivalent Simulink
models are erroneously reported as non-equivalent. This is particularly relevant
because unexpected over- or underflows due to FPA semantics can be hard to
detect, but can have profound consequences.
We illustrate the inconsistencies between rational arithmetic and FPA us-
ing the Simulink model in Figure 1. The model contains a feedback loop that
computes the consecutive sums

n

t n = i j

j =1

given the stream i 1 ,i 2 ,i 3 ,... of inputs. Furthermore, in each time frame, the
quotient

1
t n −

t n− 1
is computed. Because the inputs are constrained to the interval [1 , 5] with the
help of a Saturation block, and since t n = t n− 1 + i n , the computation of
the fraction will always succeed when computing with infinite-precision rational