Preorder relations

Abstract

We now conclude our presentation of preorder relations. We have surveyed quite a number of preorders, so before going any further a summary is in order. We have talked throughout this chapter about the following preorders: C the observational testing preorder, as a general framework presented in Section 5.2.3 ⊆ the complete trace preorder, presented in Section 5.3; ⊆CT observation preorder, the subject of Section 5.4; ⊆B (aka ⊆conv, together with ⊆may and ⊆must), surveyed in Section 5.5; ⊆R refusal preorder, presented in Section 5.6; ⊆FT failure trace preorder, in Section 5.7; ⊆ must fair testing preorder, the subject of Section 5.8; ⊆should should-testing preorder, a variant of ⊆fmust, also a pre-congruence. In addition, we have defined a generic testing scenario and the associated observable testing preorder ⊆. There exist preorders we did not consider specifically, such as Darondeau's preorder, because they were shown to coincide with preorders presented here [dN87]. We introduced trace preorders only because we had to start with something (and we decided to start with something simple), and because sometimes they make for useful comparison tools. However, trace preorders are awkward to work with, so we do not give too much thought to them henceforth. One of the comparison criteria between preorders is their power of discrimination. In this respect, the observation preorder has been shown to coincide with the generic preorder ⊆. The remaining preorders are strictly less discriminating and arrange themselves in a nice hierarchy. The only exception is the testing preorder, which is not comparable with the observation, failure trace, and refusal preorders. This is one reason for the introduction of ⊆fmust, which has its place in the hierarchy alright. This comparison has been shown throughout the chapter by examples and propositions, and is summarized in Figure 5.14. The relation ⊆fmust was also introduced because of fairness considerations (hence the name fair testing preorder). Specifically, the testing preorder deals unfairly with divergence, in the sense that divergence is reported as failure. In contrast, the fair interpretation of divergence implies that the tests succeed in presence of divergences as long as the system has a chance to eventually perform a visible action despite divergences. Since Efmust is not a pre-congruence relation, the variant ⊆should (which is the largest pre-congruence included in ⊆fmust) has also been defined. Of course, the presence of fairness, or the greater power of discrimination are not an a priori good thing; it all depends on the desired properties one is interested in. The unfair interpretations of divergence in particular are useful in differentiating between livelock and deadlock, i.e., in detecting whether the system under test features busy-waiting loops and other such behaviors that are not deadlocked but are nonetheless unproductive (and undetectable under the fair testing scenario). In terms of power of discrimination, we have noticed in Section 5.4 that the most discriminating preorder differentiates between processes that are for all practical purposes identical (see for example the processes shown in Figures 5.4 on page 130 and 5.5 on page 132). This is not to say that more differentiation is bad either, just look at the coffee machine examples from Figure 5.12 on page 141, which are in a strange implementation relation under refusal testing (only a crooked merchant would accept this) but are not comparable under failure trace preorder. Another comparison of preorders can be made in terms of the complexity of the tests and their practical feasibility. It is no surprise that the most discriminating preorder, namely the observation preorder, appears to be the least practical of them all. In this respect the award of the most practically realizable preorder seems to go to refusal preorder. This is the only preorder based exclusively on sequential tests. This being said, we are not necessarily better off since in the general case we need a number of tests to figure out the properties of the system, so that the advantage of the tests being sequential pales somehow. Another practical issue in refusal preorder is the concept of refusal itself. One can wonder how practical such a concept is. Recall that actions are an abstraction; in particular, they do not necessarily represent the acceptance of input. So how does one refuse an action without modifying the process under scrutiny itself? This does not seem realizable in the general case (whenever we cannot access the internals of the process under test). Do we take away the award from refusal preorder? In all, practical considerations do differentiate between the preorders we talked about, especially for the observation preorder which combines results in a more complex way than other preorders (that simply take the union of the results of various runs and tests) and requires a rather unrealistic concept of global testing. However, when testing systems we are in the realm of the halting problem, so practical considerations cannot ever make an a priori distinction. The utility of various preorders should thus be estimated by taking all of their features into consideration. In the same line of thought, namely practical applications, we have presented a practical framework for conformance testing based on the theory of preorders. Finally, it is worth pointing out that our presentation has been made in terms of labeled transition systems, as opposed to most of the literature, in which process algebraic languages such as CCS, LOTOS, and variants thereof are generally used. Labeled transition systems define however the semantics of all these languages, so the translation of the results surveyed here into various other formalisms should not be a problem. The upside of our approach is the uniform and concise characterization of the preorders, although we lose some expressiveness in doing so (however the literature cited therein always offers a second, most of the time process algebraic view of the domain). As well, we did not pay attention to contexts. Contexts admit however a relatively straightforward approach once the rest of the apparatus is in place. © Springer-Verlag Berlin Heidelberg 2005.