Formalization of Test Experiments
I. B. Bourdonov, A. S. Kossatchev, and V. V. Kuliamin
Institute for System Programming, Russian Academy of Sciences,
Bol’shaya Kommunisticheskaya ul. 25, Moscow, 109004 Russia
e-mail: igor@ispras.ru, kos@ispras.ru, kuliamin@ispras.ru
Received February 20, 2007
Abstract—Formal methods for testing conformance of the system under examination to its specification are
examined. The operational interaction semantics is specified by a special testing machine that formally deter-
mines the testing capabilities. A set of theoretically powerful and practically important capabilities is distin-
guished that can be reduced to the observation of external actions and refusals (the absence of external actions).
The novelties are as follows. (1) Parameterization of the semantics by the families of observable and not observ-
able refusals, which makes it possible to take into account various constraints on the (correct) interactions.
(2)Destruction as a forbidden action, which is possible but should not be performed in the case of a correct
interaction. (3) Modeling of the divergence by the  -action, which also should be avoided in the case of a cor-
rect interaction. On the basis of this semantics, the concept of safe testing, the implementation safety hypothe-
sis, and the safe conformance relation are proposed. The safe conformance relation corresponds to the principle
of independent observations: a behavior of an implementation is correct or incorrect independently of its other
possible behaviors. For a more narrow class of interactions, another version of the semantics based on the ready
traces may be used along with the corresponding conformance relation. Some propositions concerning the rela-
tionships between the conformance relations under various semantics are formulated. The completion transfor-
mation that solves the problem of the conformance relation reflexivity and a monotone transformation that
solves the monotonicity problem (preservation of the conformance under composition) are defined.
DOI: 10.1134/S0361768807050015 |
