Semantics of interactions with refusals, divergence anddestruction. Part 1. Hypothesis of safety and safe conformance

The paper discusses methods of conformance testing of the given system to the given requirements (specification) basing on formal models. The operational semantics of an interaction is designated with a special testing machine formally defining various testing capabilities. A set of powerful and meaningful capabilities reducible to observation of external actions and refusals (absence of external actions) is selected. The innovations are: 1) Parameterization of the semantics with the kinds of observable and unobservable refusals that allows taking into account various restrictions on (correct) interaction. 2) Destruction as a forbidden action, which is possible, but should not be performed in a correct interaction. 3) Modeling of divergence with a ∆-action which also should be avoided in a correct interaction. The notion of safe testing, the implementation hypothesis of safety and relation of safe conformance based on such semantics are proposed. Theoretically, test generation from specification given in arbitrary interaction semantics of the studied kind is considered.The parameterized R/Q-semantics of interaction, hypothesis of safety, safe conformance and the method of test generation proposed in this paper are the basis of the conformance theory that generalizes many of the conformances and testing methods found in literature and used in practice. Particularly, failure trace semantics and the semantics of the popular ioco relation are the instances of the R/Q-semantics. This theory is now developed in various directions. 1) Specification completion solving the problem of specification nonreflexivity in respect to conformance relation as well as the problem of safe specification traces that can not be found in conformant implementations and test traces that can not be found in safely tested implementations. 2) Monotonous transformation of the specification solving the problem of verification of the given system specification (its consistency with the components specifications). 3. Introduction of priorities into the model and the corresponding modification of conformance and test generation. 4) Propagation of suggested approach on simulations - conformances based not only on the traces of observations, but also on the correspondence of the states in implementation and specification. The issues of equivalence of interaction semantics and semantics transformations during testing using the mediator programs converting test stimuli and observations are also researched.

Keywords

Authors

References