Detail

SATEL: How to express test intentions

talk is devoted to the presentation of an integrated framework
for modeling, implementing and verifying systems with a maximum
confidence in the resulting critical system.

We will present a semi-automatic approach to test generation which
is materialized in the test intention language SATEL (Semi-Automatic
Testing Language) for CO-OPN (Concurrent Object Oriented Petri Nets).
The approach is semi-automatic in the sense that we allow the test
engineer to state test purposes (which we call in our approach test
intentions), while using unfolding techniques (introduced by Bernot,
Gaudel and Marre) for automatically finding equivalence classes of
inputs to operations of the model. While designing the test language
it was our intention to explicitly make use of the test engineer’s
knowledge in the test generation process. He/she is able to express
which parts of the model are relevant for testing and to impose
limits on how that testing should be performed. With SATEL we have
tried to devise a test generation framework that automates the
typical approach of a test engineer rather than performing an
exhaustive search of the model.

The semi-automatic aspect SATEL corresponds to the fact that, given
an operation of the model (from a black-box perspective), the test
engineer will be also be able to state that the generated tests
should include inputs that automatically cover the various behaviors
(also called in the literature equivalence classes) of that operation.

The test intentions in SATEL correspond to generalizations of the
behavior of the SUT and are expressed by writing execution patterns
with variables over sequences of input/output events of the
specification — one could also see them as testing macros. The
instantiation of these variables by the test language compiler will
yield test cases for the specified test intentions.

We have also included in SATEL support for non-determinism at two
levels. Firstly the formalism in which we express our tests is the
HML (Hennessy-Milner logic) which is a branching temporal logic. In
this way we are able to express tests which reflect non-
deterministism both at the level of the specification and of the SUT.
Secondly we have included in our language a means of treating a
specific kind of non-determinism of the SUT while it is interacting
with the environment. This is done by anticipating a reply (a
stimulation) to a given non-deterministic observation by means of a
predefined function at the level of the specification.

SATEL has been implemented in our framework CoopnBuilder environment
and we are currently validating our approach by applying it to an
industrial case study.