Open Collections

UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Coverage analysis for conformance testing of communication protocols Zhu, Jinsong 1999

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Item Metadata

Download

Media
831-ubc_1999-390136.pdf [ 7.61MB ]
Metadata
JSON: 831-1.0051312.json
JSON-LD: 831-1.0051312-ld.json
RDF/XML (Pretty): 831-1.0051312-rdf.xml
RDF/JSON: 831-1.0051312-rdf.json
Turtle: 831-1.0051312-turtle.txt
N-Triples: 831-1.0051312-rdf-ntriples.txt
Original Record: 831-1.0051312-source.json
Full Text
831-1.0051312-fulltext.txt
Citation
831-1.0051312.ris

Full Text

Coverage Analysis for Conformance Testing of Communication Protocols by Jinsong Zhu B.Sc, Tsinghua University, China, 1985 M.Sc, Tsinghua University, China, 1987 A THESIS S U B M I T T E D IN P A R T I A L F U L F I L L M E N T O F T H E R E Q U I R E M E N T S F O R T H E D E G R E E O F Docto r of Phi losophy in T H E F A C U L T Y O F G R A D U A T E STUDIES (Department of Computer Science) we accept this thesis as conforming to the required standard The University of British Columbia April 1999 © Jinsong Zhu, 1999 In presenting this thesis in partial fulfilment of the requirements for an advanced degree at the University of British Columbia, I agree that the Library shall make it freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission. Department of Computer Science The University of British Columbia Vancouver, Canada Aprils >/99j Date Abstract Generation of effective test suite and the evaluation of any given test suite are two of the most essential issues in conformance testing. We combine these two aspects and propose quantitative coverage measures that are subsequently used as the basis for generating test suites with any test coverage requirement. Two criteria for coverage measure are studied: a) fault coverage which measures the effectiveness by examining the fault detecting ability of a test suite under a certain fault model, and b) behavior coverage which measures the effectiveness by computing the amount of protocol behavior space that are exercised by a test suite. In the realm of fault coverage, we propose a coverage measure that targets on finite state specifications, typically in the form of I /O Finite State Machines (FSMs). A formal definition and algorithms that compute the measure are given. The computation of the measure is hard in general (no better than NP-complete); however, with search optimization techniques, the performance of our algorithm has been shown to be high and practical for some large protocols. The measure is then utilized to generate additional test cases to a "weak" test suite, thereby producing test suites with better coverage. The enhancement of a test suite can be done incrementally to satisfy a particular coverage requirement. The application of ii the measure in fault localization is also explored. The above coverage measure is further extended to the case of testing em-bedded modules of a composite system modeled as a set of communicating FSMs. The problem differs from the isolated module case in that the module under test has limited observability and controllability due to the presence of the test context. We propose an approach that reduces the problem to the case of isolated modules while maintaining observational equivalence at the composite system level. We prove that the calculation of the coverage measure is no better than NP-complete. How-ever, application of the measure to a real life protocol, the protocol that supports the Universal Personal Computing on the Internet, shows that at a higher level of abstraction, the approach remains effective. As a last contribution of the thesis, we studied the coverage measure for behavior coverage based on Labeled Transition System (LTS). We use the basic metric based method [100] as our theoretical foundation. We generalize the basic method to handle protocols extended with data storage in the model of extended LTS. This results in a metric characterization that incorporates the testing distance contribution from data variations. We proved that this generalized metric space possesses the total boundedness and completeness properties, which allows for a test generation and selection process that can approximate the entire protocol space with arbitrary precision. iii Contents Abstract ii Contents iv List of Tables viii List of Figures ix Dedication xi 1 Introduction 1 1.1 Motivation 1 1.2 Scope of the thesis 7 1.3 Thesis organization 11 2 Background 13 2.1 General software testing 13 2.2 Protocol conformance testing 16 2.2.1 Conformance testing system 18 2.2.2 Finite state machines 21 2.2.3 Communicating finite state machines 27 iv 2.2.4 Labeled transition systems 30 2.3 Related research 36 2.3.1 Fault coverage analysis based on the FSM formalism 36 2.3.2 Testing of Communicating FSMs 39 2.3.3 Metric based behavior coverage measure 41 3 Coverage measure for single machine testing 44 3.1 Coverage measure 44 3.2 Coverage measure calculation 48 3.2.1 Calculation of KTCM 49 3.2.2 Calculation of KSCM 58 3.2.3 An illustrative example 62 3.3 Applying the measure to real life protocols 64 3.3.1 ISDN BRI protocol 64 3.3.2 TCP connection management protocol 66 3.3.3 NBS TP4 protocol 67 3.4 More experiments 69 3.5 Incremental test suite generation 73 3.6 Fault localization 79 3.7 Evaluation of test optimization techniques 85 3.7.1 Test optimization techniques 85 3.7.2 Coverage evaluation results 90 4 Coverage measure for testing embedded modules 97 4.1 Introduction y 98 4.2 Embedded test architecture 99 v 4.3 The coverage measure 101 4.3.1 Calculation of KTCM • • • •• 102 4.3.2 Calculation of KSCM 1 1 1 4.4 Computational complexity of the measure 116 4.5 Tool set and example 117 4.6 Extension to multi-module test context 122 4.7 Testing of a universal personal computing system 123 4.7.1 The universal personal computing system . 123 4.7.2 U P C Test suite evaluation 132 5 A generalized metric based behavior coverage measure 136 5.1 Basic metric space 137 5.2 Generalized metric space 139 5.2.1 Interpretation of the distance 144 5.2.2 Example 146 5.3 Total boundedness and completeness 147 5.4 Generalized coverage measure and test selection 151 5.5 Discussion 153 6 Conclusions 155 6.1 Contributions 155 6.1.1 Fault coverage measure 156 6.1.2 Incremental test generation and fault localization 157 6.1.3 Embedded testing fault coverage 157 6.1.4 Testing of a universal personal computing protocol 158 6.1.5 Generalized coverage metric 159 vi 6.2 Future work 160 Bibliography 163 Appendix A UlO-based Test Sequences for BRI 172 Appendix B DS Test Sequences for TCP connection management protocol 177 Appendix C All T-indistingushable FSMs for the sample FSM 187 vii List of Tables 3.1 UIO Sequences for BRI 66 3.2 T C P states and their descriptions 68 3.3 Performance of C O V for some examples 72 3.4 Output sequence on G D S a for M i to M 5 82 3.5 Fault coverage results for T1-T4 91 viii List of Figures 2.1 Test architecture 18 2.2 Local test and embedded test method 19 2.3 A Finite State Machine 23 2.4 A system of two communicating FSMs 28 2.5 A hierarchy of semantics 35 3.1 Machines with respect to a specification and test suite 47 3.2 Test tree corresponding to the UIO test sequence 50 3.3 Simple backtracking algorithm 52 3.4 Domain reduction algorithm 55 3.5 Backjumping search algorithm 57 3.6 Conformance checking for deterministic specs 60 3.7 Conformance checking for non-deterministic specs 61 3.8 The two solutions for the UIO test sequence given in Figure 4 . . . . 63 3.9 ISDN BRI network layer protocol (network side at the originating side) 65 3.10 T C P connection management F S M 68 3.11 A subset of NBS Class 4 transport protocol 70 3.12 Sample FSMs used in performance experiments 71 ix 3.13 Generation of a DS for two FSMs 76 3.14 A specification F S M and its solution machines 78 3.15 The successor tree for DS generation 79 3.16 Possible faulty machines for the IUT 83 3.17 GDS tree for the example 84 3.18 A sample F S M and UIOs for each state 90 3.19 Three indistinguishable FSMs with respect to T2 94 4.1 Test architecture for embedded testing 100 4.2 Test tree construction algorithm 106 4.3 Test tree construction for embedded component 107 4.4 Proof for Theorem 5.1 109 4.5 Canonical i-cycles 110 4.6 Composition of two FSMs 114 4.7 Composition of two machines 115 4.8 A special case of E S A T 117 4.9 E C O V tool set 118 4.10 Example composite system 119 4.11 Test tree generated for the embedded component 120 4.12 Two FSMs observationally equivalent with S 121 4.13 U P C architecture 125 4.14 U P C middleware protocol 131 4.15 Test tree for the U H A 134 5.1 Testing distance between test cases A , B, and C 147 x To Yan, Shawn and Erica. xi Chapter 1 Introduction 1.1 Motivation Software testing is the primary method by which testers establish confidence in the correctness of software and achieve high software quality, whether the software is comprised of sequential or concurrent programs. There is the perception that formal program verification has a much more solid theoretical foundation than testing, it is however rarely used in practice due to the difficulty in effectively manipulating the combinatorial dimensions of many practical systems. Even taking an extremely optimistic view that verification could handle large software systems in the near future, testing would still be valuable since it validates a physical implementation in actual running environments. Moreover, in case of third party acceptance testing (say for procurement purposes) the implementation can only be analyzed by testing the product as a black box since implementation details will not be disclosed in general. The cost of testing typically constitutes about half of the overall system 1 development cost [6], and can increase significantly if the cost for corrective main-tenance is included. Significant amount of dollars are spent annually on testing in the real world of software industry. This raises the question of whether the money is well spent. In the world of software testing theory, this amounts to the issue of generating effective test suites with as fewer test cases as possible that can verify the correct behavior of an implementation. A central issue to this problem is to define an objective criterion that mea-sures the effectiveness of a test suite. The criterion must be objective since otherwise no consensus could be reached in determining the effectiveness. One cannot simply devise a measure and claim that test suites generated by this measure are superior to others. To this end, there are essentially two criteria: 1. Look at the fault coverage of the test suite, i.e., how many faults or fault types it can detect. Obviously, the more faults.that can be detected, the more effective a test suite is. 2. Calculate how much behavior space of the program is exercised (or covered) by the test suite based on a certain coverage measure. The underlying assumption is that, by covering the behavior space sufficiently, the quality of the software can be assured. The test generation methods associated with the two criteria are often called fault based testing and coverage based testing, respectively. While these two methods are fundamentally different, they are also closely related since fault coverage remains the ultimate criterion for evaluating test effectiveness [42], even when behavior cov-erage measures are considered. Both fault and behavior coverage measures provide guidance on further augmenting a test suite to satisfy the coverage criterion. 2 The most prominent fault based testing method is probably the so-called mutation testing [26, 11]. The method systematically generates a large number of small modifications of the original program (i.e., mutants) based on fault classes, and develops test suites that can kill the mutants. A test suite that can kill all mutants is considered to be adequate with respect to the fault classes. When a test suite is not adequate, more test cases can be produced to improve the test suite by killing the surviving mutants. The methodology has been well received as a systematic approach to testing. However, it is in general very computationally expensive or even impossible to compute the mutation score (the fault coverage measure that computes the percentage of killed mutants) of a test suite because a) a mutant program may be equivalent to the original program, and it is generally undecidable to determine the equivalence of two programs [26]; and b) for complex systems faults may not be enumerable. These problems can be aggravated when the method is applied to concurrent systems. Recognizing the difficulty of fault coverage measure in general software test-ing (which encompasses both sequential and concurrent program testing), we target on the area of protocol software testing, in which a protocol is modeled as a collection of finite state systems. It is a form of concurrent program testing but stressing on communication protocol properties. Within this context, many problems that were not decidable become solvable. This is a significant subset of the general software testing for two reasons: a) communication protocols are an essential part of today's information technology, and they are becoming increasingly important due to the growth of Internet and electronic commerce; and b) communication protocols rep-resent a type of interactive and concurrent systems that differ from the traditional sequential programs. We therefore developed a fault coverage measure for protocol 3 testing that is conceptually the same as the muta t ion score, but is computed i n a total ly different way. Instead of generating mutants and then k i l l i ng them, we compute the coverage measure by calculat ing the number of mutant machines that are not equivalent or quasi-equivalent (depending on strong or weak conformance testing requirements) w i t h the specification but cannot be k i l l ed by the test suite under evaluation. T h e approach also avoids enumeration of various fault classes and makes no use of the coupl ing effect assumption as i n the muta t ion testing method. The measure is first defined for the simple case where a protocol entity is tested i n an isolated way, i.e., the protocol is modeled as a single finite state machine ( F S M ) and a tester has direct access to its interface. T h e measure is then extended to the case where a protocol is modeled as a collection of communicat ing finite state machines ( C F S M ) , i n wh ich one machine is tested through a l l other machines (called test context). T h i s is often the case i n multi-layer protocols where testing of one layer can only be done v i a its surrounding layers. It is also a useful model i n dis t r ibuted : comput ing where comput ing units are dis t r ibuted i n a network, and i n embedded systems where a module is embedded i n a composite system without exposing direct access interface to the outside. T h e measure, i n b o t h isolated and embedded cases, natural ly extends to a test suite generation method that guarantees a certain (up to complete) fault coverage, and to fault local izat ion that gives accurate diagnosis to faults i n an implementat ion when it fails to pass a test suite. Due to computa t ional complexity, the above measure is best when appl ied to finite state systems w i t h smal l to medium number of states. For complex systems, the measure can be appl ied to smaller subsystems i f the system structure admits , for example, a hierarchical decomposit ion. However, there are also cases i n proto-cols - especially appl ica t ion level protocols - where da ta storage is indispensable. 4 This is tantamount to a huge number of states in a single monolithic module which would render our approach inapplicable. Moreover, in complex protocols with data storage, fault models are typically unlimited and unknown just like in general soft-ware testing. It is therefore infeasible trying to enumerate fault models and design test suites that detect them. The computational complexity required to handle a large number of fault models, even if they are enumerable, is also a major stumbling block, let alone the problem of determining the equivalence of a mutant with the original program which would typically require considerable human intervention in inspecting the mutants. This leads to a test strategy that targets on specification behavior coverage. It is based on the belief that by covering the specification of a program or protocol and eliminating faults found by coverage testing, the product quality will be assured. The coverage measure is thus focused on the coverage of the program or specification behavior space instead of the coverage of fault classes. There have been many structural coverage criteria in sequential program testing, such as statement coverage, branch coverage, and path coverage [6]. How-ever, in communication protocols, it is a challenge to define objective measures of behavior coverage that capture protocol properties,,since those general software cov-erage criteria do not lend themselves to coverage of protocol behaviors. The major difference between sequential programs and protocol systems lies in that protocols are reactive systems [81]: they receive input and produce output in a continuous in-teraction with their environment, rather than computing a single result and halting. The input domain of a protocol system is therefore a sequence which are typically infinite. This demands a different way of describing the protocol behavior space. In [100, 22, 21], a metric based test selection and coverage analysis was 5 proposed, where the protocol space is described as comprised of a possibly infinite number of execution sequences. A n execution sequence is an ordered set of events whose length may also be infinite. Event recursions are taken into account which distinguishes the method from earlier metric characterizations of protocol space [38]. When performing test suite generation and selection, the method essentially tries to cover the space by selecting a finite set of execution sequences of finite length. The beauty of the method is that by converting the protocol space into a metric space of testing distance, the selected test suites can approximate the entire protocol space with arbitrary precisions, limited only by the testing cost. The extent to which the protocol space is covered thus can be used as a measure of behavior coverage. It is proved that the test suites can achieve trace equivalence with the specification in limit, i.e., with ultimate complete behavior coverage. The metric based method uses the Labeled Transition Systems (LTS) as the underlying formalism, and nicely handles important protocol properties such as recursions, concurrent connections, and event patterns. The coverage measure also provides a quantitative definition of behavior coverage. However, it cannot handle data storage which is indispensable in most real life protocols, especially application level ones. Data storage in a protocol results in state space explosion if one simply ex-pands the protocol by unrolling the data storage into discrete values. We propose an approach to solving this problem by introducing a generalized metric space based on the Extended Labeled Transition Systems (ELTS) model, that can handle both control flow and data flow, without causing the problem of state space explosion. The space is proved to possess the important properties of total boundedness and completeness. The coverage measure is also generalized accordingly. A test genera-6 tion method is then proposed that achieves a uniform coverage within a cost limit. We also prove that the number of test cases increases exponentially with respect to the inverse of the test suite density. 1.2 Scope of the thesis The objective of this thesis is to develop formal, objective, and effective coverage measure of test suites for communication protocols. We explore the issue of coverage measure from the two aspects as mentioned in the previous section: fault coverage based on the F S M and C F S M model, and behavior coverage on the LTS and E L T S model. The two coverage measures can be applied to systems that range from small, medium size protocols, which are typical for control protocols, abstracted and decomposed protocols, to complex monolithic protocols with large data space. The combined use of the measures provides a methodology that can handle a wide spectrum of protocols. In the area of fault coverage, we developed a measure that is similar to the mutation score in mutation testing but is approached from the standpoint of machine identification. The measure evaluates the fault coverage of a given test suite, which is considered as constraints which a mutant F S M must satisfy in order not to be detected. The number of these FSMs that are not equivalent to the specification F S M is used as the coverage measure. Since we restrict ourselves to FSMs, the machine identification problem is decidable [18], i.e., a machine can be inferred from its finite external behavior, as long as the number of states is upper bounded. Moreover, the equivalence of two FSMs can be determined efficiently, as opposed to the undecidability of general program equivalence problem. Although the measure is computable, the computation is unfortunately no 7 better than NP-complete, as it depends on a known NP-complete problem [37], just like many real problems. To improve the computational efficiency, we employed techniques developed in the area of artificial intelligence, which can dramatically improve search efficiency for a constraint satisfaction problem. The techniques in-clude domain reduction before the search, and backjumping and dynamic pruning during the search. The problem is formulated as a constraint satisfaction problem, where the machines that can pass the test suite are the solutions for the problem. Domain deduction eliminates many possibilities before the search, while backjump-ing directly goes back to the source of search failure, thereby saving time during backtracking. The deterministic properties of FSM are also used to dynamically prune the search space. We developed a tool called COV, which allows evaluation of fault coverage of a given test suite against its specification written in the FSM formalism. It can handle both complete and partial specification machines. A coverage measure is calculated by computing faulty machines that cannot be detected by the test suite. The tool can also be used to augment a test suite by adding more test cases that distinguish the faulty machines. The augmentation achieved is determined by what coverage is required of the test suite, up to 100%, i.e., a complete test suite. Fault localization can be done by using the I/O behavior of the faulty machine as the initial test suite for COV and adding more test cases to distinguish the fault suspects. Using the tool, we have performed various experiments. The results were encouraging in that a sizable real protocol, the NBS Transport Class 4 protocol (the predecessor of the ISO Transport Class 4 protocol), can be handled in a reasonable amount of time. We have also used the tool to analyze a number of test sequence optimization techniques and confirmed that optimization may possibly reduce the 8 fault coverage of a test suite. The basic results were reported in [108, 109]. Since the original algorithm used strong equivalence as the conformance relation, it was only applicable to completely specified FSMs. The extension of the measure to allow the notion of conformance in the context of partial or nondeterministic machines is new in this thesis. Our measure is extended to embedded system testing and translated into the problem of machine identification in context. This has many applications in multi-layer or multi-module protocol testing and distributed object testing. It also makes our method applicable to decomposable protocols so that the cost for test generation and evaluation is reasonable. We developed a method that builds the embedded module based on a global test suite using reachability computation. Due to the limited observability and controllability of the embedded module which is surrounded by a test context, equivalence of mutants has to be determined at the composite system level, which is what a tester can access. We prove that the equiv-alence can be determined in polynomial time; however, the determination of the existence of an embedded mutant machine that satisfies a test suite remains NP-complete. Therefore the calculation of the coverage measure is in general a hard problem. A tool called E C O V is developed to demonstrate our ideas and concepts. It accepts global system description as a set of communicating FSMs, and generates test trees that correspond to the embedded module. The construction of mutants from the test trees is done by the tool C O V . The tool is applied to a real life multi-module protocol, the universal personal computing (UPC) system, and demonstrates the methodology. The tool can be further used to enhance a test suite based on coverage requirement. 9 As complete fault coverage is often too demanding for any non-trivial proto-cols with a non-trivial fault model (the length of test suite tends to be exponential with respect to the number of states), we consider behavior coverage as a viable alternative where extensive exercising of the behavior space is desired, e.g., for high reliability. The advantage of behavior coverage becomes more evident for protocols with data storage, where F S M based methods are infeasible due to state space explo-sion. In such a case, extended LTS (with data) turns out to be a convenient model where various extensional equivalence relations can be employed as the conformance relation. Our work in this area is based on the basic framework proposed in [100, 22], where a metric characterization was introduced upon the behavior space. We extend the results to the realm of extended labeled transition systems where data storages are included. A new generalized metric space is defined, in which contributions to testing distance by data valuations are incorporated in a way that no state space explosion will be resulted. We proved that the space is both totally bounded and complete. This makes it possible to select a finite test suite that covers the entire space. A test generation and selection algorithm is proposed, and a generalized coverage measure is defined. We also show that the number of test cases increases exponentially with the inverse of the test suite density. This may be seen as a negative result but it is an evidence that in general it is very hard to achieve high reliability by testing, e.g., the exponential length of the W method [19], and in the field of "ultra-high dependability" [65]. 10 1.3 Thesis organization The rest of the thesis is organized as follows. Chapter 1 provides the background material for our methodology. Major results related to our work in general software testing theory are summarized.. These provide a foundation for protocol software testing. Due to the special properties of interactive systems, protocol testing the-ory, while inheriting from general software testing theory for basic concepts and methodology, develops its own abundant theories that focus on concurrent, commu-i nicating and nondeterministic processes. The theory of conformance testing is then reviewed which lays a fundamental framework in which our work fits. The emphasis will be placed on the various conformance relationships developed for finite state systems including the models of F S M and LTS. The coverage measures depend on the conformance relationships because they determine whether or not a mutant is considered as a conforming implementation of the specification. The coverage measure based on machine identification is developed in Chap-ter 3. Algorithms and tools are presented along with an empirical study of the performance of the algorithms, including the application to three practical proto-cols (ISDN BRI, T C P connection management, and NBS Transport Class 4). The measure is then applied to the area of test suite generation and fault localization. The chapter concludes with an evaluation of a few test suite optimization techniques in the literature. The measure for embedded system testing is described in Chapter 4. The measure remains based on machine identification, but due to the presence of test context, new issues must be solved. Algorithms that solve the problems are detailed with an analysis of computational complexities. The problem to find an embedded mutant that accepts the given test suite is shown to be NP-complete as expected. 11 We then apply the measure to the testing of a universal personal computing (UPC) protocol. The protocol is modeled as a communicating F S M system, and one of the F S M is tested as an embedded module. The application demonstrates the usefulness and the practicality of the measure. In Chapter 5, we finally look at the behavior coverage issue for extended LTS systems. This chapter first reviews the basic metric based coverage model that applies to pure LTS systems, and then proceeds to propose a generalized metric based coverage measure applicable to extended LTS systems with data extension. Properties of the generalized metric space are proved, along with a generalized test selection algorithm. This allows the metric based method to be applicable to protocols with data storage. The last chapter concludes the thesis by giving our contributions as well as some future work. 12 Chapter 2 Background We present some background material in this chapter in order to put our work in perspective. We start by giving an overview of related theory in general software testing that defines testing systems and test data adequacy. Protocol conformance testing, a branch of testing where an implementation of a protocol is tested against its specification, is then presented. This lays a theoretical setting for the subsequent chapters. We close by discussing some related research work. 2.1 General software testing Software testing aims at achieving confidence that a software system works correctly. This confidence is ordinarily established by executing the software on test data chosen by certain testing procedure. A simple programming context is often assumed in software testing theory [43]: program has a pure function semantics where the program is given a single input, and computes a single result and terminates. In this context, a test is a single value of program input, which causes a single execution of the program. A test set 13 is a finite collection of tests. We also call it a test suite, as is often used in protocol testing. This model does not reflect well interactive and concurrent systems but can be adapted if we consider their test suite as consisting of tests made of sequences of inputs. Each program has a specification that defines an input-output relation. A program P satisfies its specification S for input x (denoted P satx S) iff: if x G dom(S) then on input x, P produces output y such that (x, y) G S. A program P is correct with respect to its specification S (denoted P corr S) iff it satisfies S on all inputs, i.e., P corr S = d e f Vrr € dom(S) : Psatx S. A program P with specification S fails on input x iff P does not satisfy S at x.. Denote the set of all programs V (P G P), the set of all specifications S (S G S), and the set of all tests T (T € T). A testing system can be defined as [40]: Definition 2 . 1 (Testing system) A testing system is a quintuple (V, S, T, corr, sat) where P,S, and 7~ are arbitrary sets of programs, specifications and test sets respec-tively, corr C V x S, sat C T x V x S, and VPV5VT : P corr S => P satT S. That is, in a testing system, if a program is correct with respect to its speci-fication, then no tests of that program will ever fail with respect to the specification. Since we wish to verify the correctness of a program by testing, it is interesting to see if there are finite test set T such that P satr S => P corr S. Such a test set is called reliable [50]: Definition 2 . 2 (Reliable test) If P is a program that implements specification S on domain D, then a test set T C D is reliable for P and S if V i G T : P satt S VteD : P sat* 5, i.e., P corr S. 14 Howden showed that finite reliable test sets exist, however there is no effective procedure to generate them [50]. A n alternative testing criterion proposed by Budd and Angluin is test adequacy [12]: Definition 2.3 (Adequate test) If P is a program that implements specification S on domain D, then a test set T C D is adequate for P and SifV programs Q : Q -.satr, S =4> 3t 6 T : Q ->satt S. In other words, a test set is adequate if it causes all incorrect versions of the program to produce an output that violates the specification. This definition is appealing in that it requires test sets to detect faults rather than show correctness. However, again there is no effective procedure to either generate adequate test sets or decide whether a given test set is adequate. The reason is that this amounts to requiring tests to distinguish a correct program from all possible incorrect programs, which is clearly undecidable. 1 Due to this difficulty, a criterion called relative adequacy was proposed [26]: Definit ion 2.4 (Relatively adequate test) If P is a program that implements specification S on domain D, and 3> is a finite collection of programs, then.a test setT C D is adequate for P relative to $ if V programs Q 6 $ : Q ->sat£> 5 =4> 3t € T : Q -.satj S. That is, a relatively adequate test set causes a specific, finite number of incorrect versions of the program to fail. This makes test generation easier since we can focus on that specific (finite) set of incorrect programs and devise test sets that can distinguish them. Unfortunately, although this makes the problem more tractable, we still cannot always find procedures for generating relatively adequate test sets. 15 The above results are useful in that they tell us what we can and cannot gain from testing. In general we cannot show correctness through testing and we cannot generate reliable or adequate test sets. On the other hand relatively adequate test sets do exist, and in this thesis we show that in the specific context of protocol testing, we do have a workable procedure to generate relatively adequate test sets and to decide whether a given test set is relatively adequate. Moreover, when relative adequacy is still too expensive, coverage measure can be defined and calculated to measure the degree of adequacy. This gives testers a clear idea of how good a test set is. 2.2 P r o t o c o l conformance testing In software testing, a distinction is made between structural testing and functional testing. Structural testing examines the internal structure of an implementation and aims to exercise the program text as thoroughly as possible. Tests are derived from the program code by criteria such as statement coverage and path coverage. It is also referred to as white-box testing and is mostly used in in-house program development and debugging. In functional testing, testers are not given access to the program code; only the specification is given. Testers can only design test sets from the specification and determine the correctness of the implementation from its response to the tests. This is also called black-box testing since no internal structure of the implementation is accessible. It is therefore mostly used in third-party testing1. Protocol conformance testing is a kind of functional testing. Communication protocols are a common set of rules and conventions used by communicating parties 'Of course, this does not prevent the vendors from using the method to test their product before selling or submitting for certification. 16 in a networking environment. Typically, a protocol is standardized in a specification document which contains details on the rules and conventions, and what services (functions) it provides. Implementations are then derived from it. Conformance testing serves as ensuring that an implementation does conform to the standard, so that implementations derived from the same specification may interoperate with each other. Research in protocol conformance testing thrived in the last decade due to the fast development of computer networks, and perhaps most importantly, to the considerable ISO standardization efforts in conformance testing, including test archi-tecture, test methodology, and the use of formal methods in testing [82, 52, 55, 54]. This aroused a lot of research interests in the area. It was closely associated with the ISO/OSI architecture since conformance testing is believed to be the primary method in assuring interoperability of different implementations of the same stan-dard protocol. It also allows certification of OSI-compliant products from various vendors. Today, ISO/OSI activities have mostly died out, won over by the success of the Internet. However, we maintain that the OSI conformance test methodology remains a useful framework that can be applied to any protocol testing. To be fair, it also lays a solid foundation for conformance testing research as well as practical testing activities. It should be noted that, in addition to conformance testing, there are also other types of protocol testing, such as interoperability testing which determines if two implementations actually interoperate, performance testing which measures the performance of an implementation such as throughput and responsiveness, and robustness testing which determines how well an implementation recovers from var-ious error conditions. These are very important to assure the quality of protocol 17 software, but they are out of the scope of this thesis. 2.2.1 C o n f o r m a n c e tes t ing sys tem The generic test architecture for conformance testing is shown in Figure 2.1. The components of the architecture are: test interface (or context) tester PCOs Figure 2.1: Test architecture 1. a tester; 2. an implementation under test (IUT); 3. test interface (also called test context); 4. points of control and observation (PCOs); 5. implementation access points (IAPs). The tester contains a test engine that executes test suites by applying test cases and observing the IUTs responses at the PCOs. Each application of a test 18 upper tester lower tester (a) Local test method (b) Embedded test method Figure 2.2: Local test and embedded test method case t is called a test run. It results in a verdict of pass, fail, or inclusive, i.e., the determination of the relation satj. This generic architecture encompasses the various test methods as defined in [52], depending on the distribution of the tester and IUT access points (PCOs and IAPs). For example, the local test method where the tester has full access to the IUT, i.e., IAPs are PCOs, and the embedded test method where test interface surrounds the IUT (Figure 2.2). The tester can be split into upper and lower testers and may be distributed in different systems (in which case a test coordination pro-cedure is needed to synchronize the two testers), and P C O s may also be positioned at a system different than the IUT, such as via a network service provider. 19 Protocol conformance testing can be formalized as in [95]. However, for our discussion, it suffices to use the simple program model in Section 2.1. Here we define a protocol as a function that computes an input sequence and produces an output sequence. We redefine the sat relation to reflect the meaning of conformance relation in a protocol testing context. Let S be a protocol specification and I an implementation of S. A n input sequence X is said to be in the domain of S if it is accepted by S, i.e., S admits X and produces an output sequence within finite time. I satisfies S for input sequence X iff: if X G dom(S), then on input sequence X, I produces output sequence Y such that (X, Y) € S. I conforms to S if I satisfies S on all input sequences accepted by S. Although this modeling of protocols as a function is simple and generally not enough to study the finer properties of protocols such as communications and concurrency, it makes it possible to understand that the negative results in software testing should carry over (if not worse). So we don't try to do the impossible, and focus on working out practical tests that are at most relatively adequate. In the following sections, we'll summarize two formalisms widely used in pro-tocol testing and the associated conformance relations which is a further refinement of the sat relation in the context of protocol testing. The first is the F S M model which is typically used in fault coverage analysis, and the second is the LTS model which will be used in our behavior coverage analysis. The conformance relations provide a ground for further discussion of fault and behavior coverage. 20 2.2.2 F in i te state machines Finite state machine is a well known formalism for modeling finite transition systems. It has been widely used to model systems in many areas such as sequential circuits [34, 33, 59], compiler theory [4], and communication protocols [7, 49]. The research on the subject of finite state machine testing and fault detection can be dated back to the 50's, when Moore first introduced the testing framework [71]. The problem was formulated as determining the state transition diagram of a machine (with known number of states) by performing experiments on it. Many results were generated, mostly targeted on testing sequential circuits [45, 39, 59]. Since the testing problem in communication protocols is essentially the same when the control part of a protocol is modeled as an F S M , the research resurfaced and thrived in the area of communications protocol testing [88]. Some old results obtained for switching circuits were dug out or rediscovered, and new results as well as extensions to handle special protocol testing problems were produced. This has been an active research area in the last decade. We start with a general definition of the (single) F S M model, which admits both deterministic (DFSM) and non-deterministic (NDFSM) machines. Definition 2.5 (FSM) An FSM is a 7-tuple M=(Q,X,Y,s0,S,X,D) where Q is a finite and non-empty set of n states {qo, ...,qn-i} with qo as the initial state; X, Y are the input, output alphabet respectively; 5 : D —> 2^ is the state transition function; A : D —» Y~ is the output function; D is the specification domain of M, i.e., a subset of Q x X. 21 If |t5(t7,x)\ = 1 for all (q,x) G D, M is said to be deterministic, i.e., for the same input at any state, the machine transfers to one and only one next state. If D = Q x X, M is said to be completely specified or complete, otherwise it is partial. Domain D is sometimes omitted when there is no ambiguity. For deterministic machines, the functions 5 and A are naturally extended for an input sequence a = x\X2...xt:. S(qi,a) is the final state after a is applied to state qi, and X(q\,a) denotes the corresponding output sequence. That is, X(qi,a) = VWi-Vk where yt = X(qi,Xi) and qi+i = S(qi,Xi) for i = 1, ...,k, and 6(qt,a) = qk+i-Also denote 5(q\,o) = qk+i by q\ A qk+i- Input sequence a is called an acceptable input sequence for state qi G S if there exists k states qn,qi2, •••,qik € S and an output sequence A(c7ji,cr) = y\V2---yk G ^ * such that there is a transition path qn Xl-^/1 qi2 X21$2 ... Xkl$k qik yVe call a/X(qi,a) an acceptable sequence for state qi G Q. For illustrative purpose, an F S M is often drawn as a directed graph G = (V, E), where the vertex set V denotes the set of state, and the edge set E represents the transitions, i.e., V = {q0,...,qn-i},E = {{qi,qj)\3x € 1 ^ 4 qj}. A n edge from qi to qj, which receives input i and produces output o, is often labeled by (qi,qj',L) where L = i/o, or simply L. Figure 2.3 shows an example (the initial state is doubly circled). During F S M testing, we want to determine whether an implementation of i a system conforms to its specification, both represented as an F S M . To define a conformance relation between two machines, we need to define some relations. In the following definitions, Let A — (SA, X, Y, 6A, XA, DA) and B = (SB, X, Y, SB, XB, DB) denote two FSMs having the same input and output alphabet. 22 Figure 2.3: A Finite State Machine Definition 2.6 (V-equivalence) Let qa and <j(, be two states in A and B, and V a set of input sequences. qa is said to be V-equivalent to qb, denoted qa =y qt,, if A and B produce the same output sequence when each input sequence in V is applied to them. Otherwise, A and B are said to be V-distinguishable, denoted qa Qb-Definition 2.7 (Equivalence) Let qa and qi, be two states in A and B. qa is said to be equivalent to qi, if qa is V-equivalent to qi, for any set of input sequence V. These two definitions give the meaning of equivalence for two states. They are equivalence relations as they are reflective, transitive and symmetric. The equiv-alence relation between two machines are defined based on them. Definition 2.8 (FSM equivalence) Two FSMs A and B are V-equivalent (equiv-alent), denoted A =v B (A = B), iff SA and SB are V-equivalent (equivalent). This states that two machines are equivalent if and only if they produce the same output sequence for all input sequences. For two machines that have different alphabets, [79] extends the definition of V-equivalence to allow the common set of the two machines' acceptable input sequences, i.e., V C X*AC\XB, where X*A and XB denote the set of all acceptable input sequences for machine A and B respectively. 23 F S M equivalence relation is widely accepted as a conformance relation in protocol testing, and is often termed strong conformance. For incompletely specified (i.e., partial) machines, a quasi-equivalence rela-tion [75] needs to be defined. Definition 2.9 (Quasi-equivalence) Machine A is said to be quasi-equivalent to B, denoted A^B iff and Vcr G Xg : X(SA, a) = X(SB, a)-Note that quasi-equivalence is not an equivalence relation since it is not sym-metric. In protocols, many transitions are often not explicitly specified in a specifi-cation. Quasi-equivalence allows to consider implementations that make intelligent decisions on unspecified transitions yet remain to be conforming. As pointed out in [75], unspecified transitions in a partial machine may have different formal meanings as to their "undefinedness": 1. Implicitly defined: A n unspecified transition is completed by certain complete-ness assumption. Commonly used assumptions are: a) a loop transition with null output is added; b) a transition to an error state with an error output is added. This assumption is based on the fact that implementations should be a complete machine without refusing any input; therefore if an expected input arrives it should either ignore it or output an error message. 2. Undefined by default: Under this assumption, an unspecified transition is considered as might be any subset of Q x Y. This represents a notion that implementations are given a flexibility in implementing one of the options [74]. 3. Forbidden transitions: This states that an unspecified transition represents the case where the transition is not allowed to be executed for a system. This may 24 be because of system environment restrictions that make the events impossible to happen. Quasi-equivalence relation is particularly useful in handling the second case. It is also called weak conformance since only the core behavior of the specification machine, i.e., the defined transitions, is concerned for a conforming implementation. The first and third cases are actually equivalent to completing the partial machines with additional transitions so the equivalence relation (strong conformance) can be used. To handle non-deterministic machines, we use the following reduction relation as our conformance relation. A conforming implementation is thus a deterministic reduction of B. Definition 2.10 (Reduction) Machine A is said to be a reduction of B, denoted A< B iffX*A D X*B and Ver £ XB : \{SA, o) C X(SB,a). In summary, we use the equivalence and quasi-equivalence relations as the conformance relation for deterministic FSMs, and the reduction relation for non-deterministic FSMs. Definition 2.11 (Conformance) A is said to be conforming to B, denoted A conf B, iff 1. If B is a deterministic FSM, then A and B are equivalent or A is quasi-equivalent to B, i.e., A = B V A >; B; i 2. If B is a non-deterministic FSM, then A is a reduction of B, i.e., A < B. 25 We can derive relatively adequate test cases based on the relations. First of all, the space of all possible implementations of an F S M specification must be limited. This results in a finite space of mutants which a relatively adequate test suite must be able to kill. The way the mutants are defined is called a fault model. Formally, Definition 2.12 (Fault model) A fault model T for the domain V is a mapping T : T> —> V(V), where V(T>) is the power domain ofD. A test suite is a finite set of acceptable sequences for the specification F S M . Denote the space of mutants as M.. Using the conformance relation defined in Definition 2.11, we can define a relatively adequate test suite T as follows. Definition 2.13 (Relatively adequate test suite) A test suite T is said to be relative adequate for a specification S iff\/lEM:I =T S => I conf S. In protocol testing, relatively adequate test suite is also called a complete test suite, with the understanding that it is only relatively complete where the mutant space is finite under some assumptions (for example, the number of fault classes is limited). The following fault classes and their combinations are often used in protocol testing based on a single F S M . 1. Single output fault: change the output of a transition; 2. Single transfer fault: change the tail state of a transition; 3. Single extra transition: add a transition; 4. Single extra state: add an extra state. 26 They may be combined to generate more complex faults. However, we should note that the fourth operation should not be applied excessively, as this will increase the number of all possible implementations exponentially. Typically, we assume an upper bound for the number of states in implementations, in order to limit the mutant space to a reasonable size. Given a fault model, which in effect defines the set of all possible implemen-tations of the specification machine, fault ^coverage can be defined as a percentage of faulty implementations that can be detected by a test suite. When all faulty machines can be detected, the test suite is complete with respect to the fault model. The corresponding coverage measure is 100%. 2.2.3 Communicating finite state machines The finite state machine model is used to specify one protocol entity in an isolated way. For complex protocol systems, it is necessary to model them as a collection of communicating modules, each one modeled as a single F S M . The F S M modules communicate by a full-duplex, error-free, FIFO channel, i.e., the communication model is asynchronous. The synchronous model requires that the communicating parties are engaged at the same time in order for a communication to happen. It can be considered as a special case of asynchronous communication with a queue capacity of zero slots. Therefore, in this thesis we focus on the more general case of a fully asynchronous communication between the component machines. Suppose there are TV finite state machines Fi = (Qi,Xi,Yi,qoi,5i,\i,Di), where i = 1 , N . A system of communicating finite state machines (CFSM) com-posed of the N FSMs can be defined as follows. Definition 2.14 ( C F S M ) A system of communicating finite state machines is a 27 quadruple ((Qi)f=1, (goi)iLi, (Mij)i,j=n A,A) w h e r ^ • (Qi)iLi a r e N disjoint finite sets with Qi representing the set of states of Fi, • qoi G Qi is the initial state of Fi, • {Mij)^j=Q are (N + l ) 2 disjoint finite sets (with Ma empty for all i), where M{j represents the messages that can be sent from Fi to Fj, • A is a state transition function for each i and j: Qi x Mji —>• Qi, • A is an output function for each i and j: Qi x Mji —>• Mj£ for some k. For the purpose of testing, we define messages that represent the interactions of the C F S M and a tester as external actions. External inputs are messages sent to the C F S M by the tester, while external outputs are in the opposite direction. Messages exchanged among the component machines are internal actions, input or output with respect to a machine in question. In the above definition, queues for external input are denoted MQJ while external output queues are M J Q . 1 x l , x 2 - M01 M12 ^ u 2 / z l ul,u2 x2/ul zl/ul xl/ul ^ - ^ ) d / u 2 z2/u2 zl/yl x2/y2z2/yl MW M21 " 1 / Z l / \ u 2 / z 2 u2/zl ul/zl \ Fl F2 yi.y2 Figure 2.4: A system of two communicating FSMs 28 Figure 2.4 presents an example C F S M composed of two communicating FSMs where N = 2, Q i = {a,6}, Q2 = {1,2,3}, i7oi = a,q02 = 1, Moi - {0:1,0:2},Mio = {2/i,X/2>, M12 = {ui,u2},M2i = {zi,z2}, A(a,x\) = a, A(a,xi) = u\, A ( l , u i ) = 2, A( l ,u i ) = z\, etc. Properties of a C F S M are denned in terms of its execution. A n execution is a sequence of global states starting from the initial state by means of reachability com-putation [103, 9] (also called composing). A global state is defined as a pair (Q, C), where Q is an iV-tuple <ZJV) (qi £ S{ for i — 1,...,N) and C is an iV 2-tuple ( c n , C I J V , C 2 1 , C J V J V ) , where Cij is the contents of the queue for messages from F{ to Fj, i.e., sequence of messages from Mij. One step of execution is determined by a message exchange between any two component FSMs. Depending on the message queue states, a global state can be divided into two categories: stable and transient. In a stable state, at least one component machine is waiting for an external input, i.e., its inputs queues are empty; otherwise the state is transient as it will quickly transfer to another state without outside intervention. Al l global states of a C F S M and the transitions among them constitute a single composite machine. Such a composite machine is often denoted as a product of its components: F i x ... x Fpf or ILf^Fj where product indicates composing by reachability computation. For conformance testing, we assume that only stable global states can be 29 observed. Therefore internal actions in the composition machine should be hidden to give a global behavior that is visible to a tester. We call such a simplified composition machine a global machine. Due to this limited visibility, the conformance of a C F S M must be determined at the global machine level under the observational equivalence relation [1], regardless of whether all modules or just one module is being tested. Moreover, the so-called I/O ordering constraint [78] is often assumed that requires an external input be applied to the system only when it has reached a stable state. This makes it possible to generate a global machine with much reduced number of states and makes conformance testing more tractable. However, this assumption reduces the tester's capability in testing system behaviors under concurrent external actions. In practice, we often try to avoid composing CFSMs because this would cause the state-explosion problem. In protocol testing, there are methods that aim at producing a reduced composite machine and then testing it as a single F S M [67].' In this thesis, however, we focus on testing each component individually so that the composite system can be tested successively. This avoids the problem of state explosion when a system is structured as communicating components. 2.2.4 Labeled transition systems Labeled transition system (LTS) is another widely used semantics model in protocol specification and testing. It is a structure that consists of states with transitions between them, and the transitions are labeled with actions. Different from the F S M model, this formalism is based on process algebra which offers an abundance of operators, a rich algebraic structure and a well developed fixed point theory [98]. The most fundamental difference with F S M is the distinction between input and 30 output actions, which is crucial in F S M model but absent (on the semantical level) in LTS. No distinction between input and output is made in LTS. Moreover, all actions in LTS are under control of both the system and its environment and must be executed simultaneously, i.e., the interactions are rendezvous in nature. LTSs are often not fully specified; those unspecified interactions are considered not possible or deadlocked. LTS can be used to model the behavior of processes, and serves as a semantics model for various formal specification languages, such as'CCS [70], CSP [48], and L O T O S [8]. Extensive work has been done on testing theory based on LTS, see for example [31, 10, 73, 60, 80, 96]. Various implementation relations are defined between a specification and its implementation, which form a theoretical foundation for test generation and coverage measure. Formally, a labeled transition system is defined as follows [96]. Definition 2.15 (LTS) A labeled transition system is a 4-tuple (S,L,T,SQ) where • S is a countable, non-empty set of states; • L is a countable set of labels; • T C S x ( L U {T}) x S is the transition relation; • so G S is the initial state. In the definition, L represents the set of observable interactions and the special label r represents an unobservable internal action. In communications pro-tocols, we often limit ourselves to strongly converging LTSs, i.e., ones that do not have infinite compositions of transitions with internal actions. 31 Similar to the FSM model, we can also define a trace of an LTS as a finite sequence of observable actions. The set of all traces over L is denoted L*. Further notations are defined as follows. Definition 2.16 (LTS notations) Let p = (S, L,T, SQ) be a labeled transition sys-h s,s' 6 S, and let Pi G L U { T } , a, G L, and a eL*. 5 A s' = d e f {s,n,s')ET s — • S = d e f 3 s Q , s n : s = so ^ s\ ^ •••^sn = s' HI—fin = d e f 3s : s = s —> s fll—fln s = d e f -, / Hl-'-ffn i -ids : s = s —> s s4>s' = d e f s = s or s —> s s^s' = d e f 3si, S2 : s si A S2 s' s am-n s' = d e f 3so, —,sn : s = so Q si ^ • • • % s n = s' s^ = d e f 3s': s^ s' a = d e f - 3 s ' : s ^ s ' Trace(p) = d e f {oEL*\p^} In order to handle protocols with data flow, we need to extend the basic LTS to include data. Here we define an extended LTS (ELTS) as having data values in the action label. Definition 2.17 (ELTS) An extended labeled transition system is a 4-tuple (S, L, T, so) where • S is a countable, non-empty set of states; • L is a countable set of labels each of which consists of an action name and a set of data values for the data parameters associated with the action; 32 • T C S x (L U {T}) x S is the transition relation; • so G S is the initial state. This is the E L T S we will be using when defining our generalized metric space for behavior coverage analysis (see Chapter 5). We have left out the conditions part often defined for a transition in extended LTSs, since we handle that part separately from our metric based test selection, where the conditions that test data must satisfy are determined out of the metric space. Conformance relations Based on the above formal model, we can discuss conformance testing in an environ-ment modeled as labeled transition systems. Before doing so, a few concepts need to be defined. We follow the formal approach to conformance testing in [95, 96], and define the concept of test case and test suite as follows. Definition 2.18 (Test case) A test case t is a 5-tuple (S, L,T,v, so) is a deter-ministic labeled transition system with finite behavior, and v : S —> {fail, pass} is a verdict function. The class of test cases over actions in L is denoted by CTSt{L). Definition 2.19 (Test suite) A test suite T is a set of test cases: T G V{CTSt{L)), where V{CTSt{L)) is the power set of CTSt(L). Two points merit our attention in Definition 2.18: 1) a test case should be finite since it must be finished within a finite time, and 2) it should be deterministic, since during testing a tester should know what it's going to do. At a higher level of abstraction, this may sound not necessarily the case, since for example, a tester 33 may determine the next action depending on a particular condition, say a data value returned by the IUT. However, this determinism is generally true when a more microscopic view of test events (with data valuations, for example) is taken. A test run in LTS is often modeled by a synchronous parallel execution of a test case with the IUT, which continues until a deadlock occurs, i.e., no more interactions are possible. At this point, if the verdict of the test case in the state is pass (or fail), then we say the IUT passes (or fails) the test case. Conformance testing is based on test runs that apply test cases to the im-plementation as a black box. Since intensional properties of the implementation is not accessible, we must use extensional equivalence relations as the conformance relation. There are many extensional equivalence relations defined in the literature, e.g. [73, 35]. The semantics of the relations determines whether an implementation conforms to its specification, by stating which aspects of the system behavior are of interest in a particular environment. Depending on the properties of a tester and the interface between the tester and the implementation, different semantics can be defined. A spectrum of the semantics is reproduced in Figure 2.5 [75, 35]. In this hierarchy, the finest model with the strongest assumption about test-ing environment is the bisimulation semantics, while the coarsest model with the least assumption is the trace semantics. Simulation based semantics often requires that there be multiple copies of the IUT after a trace has been observed, and the tester be able to observe them independently [75]. In our work, we will use the trace semantics as our model, since we consider it as the most practically feasible one. Under such a model, the conformance relation can be defined as: Definit ion 2.20 (Conformance) Let B\ and B2 be processes. B\ conf B2 iff 34 bisimulation semantics I 2-nested simulation semantics ready simulation semantics trace semantics Figure 2.5: A hierarchy of semantics Vi G L* : t € Trace(Bl)ifft E Trace(B2). This definition essentially says that B\ conforms to Bi if and only both processes have the same set of traces. This applies to the E L T S as well. We use this definition as the conformance relation in this thesis. Test derivation Work on testing systems modeled as labeled transition systems has been focused on testing the conformance relation between an implementation LTS and its speci-fication LTS. The concept of canonical tester was introduced in [31]. Informally, a canonical tester of a specification S may test all the traces of S, and it deadlocks with, and only with, the processes that are not abstract implementations of S. For an S with infinite behavior, its canonical tester is also infinite. This makes selection 35 of finite tests an important issue. Also, it is challenging to meaningfully measure the coverage of a finite test suite against an infinite behavior. There has not been much work done in this area. The most prominent piece of work is probably the metric based test selection and coverage measure by Curgus and Vuong [100, 22]. There is also work that attempts to convert an LTS into an F S M under some kind of equivalence relations, for instance trace or failure equivalence, and then use well-developed methods in F S M testing to attain a satisfactory fault coverage [13, 75, 91]. This is an interesting effort in applying existing methods in one formalism to another. However, in this thesis we choose to directly work on the LTS model when behavior coverage is considered, for its rich algebraic structure and easy handling of non-determinism and concurrency. 2.3 Related research Since test generation and coverage evaluation of test cases are the core issues in protocol testing, there has been a great deal of research in the area. We summarize some of the most closely related work in this area which has been an inspiration to our research. 2.3.1 Fault coverage analysis based on the F S M formalism Fault coverage evaluation of a given test suite computes how many faulty machines can be detected. A faulty machine is defined as one that deviates from the behavior as defined in a specification with respect to a certain fault model. It is also called a non-conforming machine of the specification. The most widely used fault model is the "up-bounded number of states" model, which assumes that the number of states in an implementation does not exceed an integer greater than or equal to the 36 number states in the specification, and the implementation possesses the same input alphabet as the specification. Let the upper bound of the number of states be m, the specification be Ms, and the given test suite be T . The fault coverage is then a function of m,Ms and T. Denote it as FC(m,Ms,T), or simply FC(T) when m, Ms are obvious. A straightforward approach would be to calculate all FSMs with a given in-put/output alphabet and an upper bound of the number of states, and then test them against the test suite. However, there are (m\Y|)mlxl FSMs with m states, | X | inputs and \Y\ outputs, and the number of distinguishable machines asymptotically approaching (m\Y\)m\x\/m\ [44]. It is obviously impossible to examine all machines when m\X\ is large. A n earlier attack to this problem is to use the Monte-Carlo sim-ulation method [24, 90]. The idea is to randomly generate, say k, mutant machines by applying fault operations to the specification, and then execute them against the test suite to see if they can be detected as faulty. If a mutant passes the test, it is further checked whether it conforms to the specification. Suppose there are k\ mutants detected, and k2 mutants actually conform to Ms, FC(m,Ms,T) would be approximately k\/(k — k2)- In fact, FC(m,Ms,T) = lim A disadvantage of the simulation method is that large number of mutants must be generated and executed against the test suite. Yao, Petrenko and Bochmann [107] proposed a structural analysis method which avoids the generation and execu-tion of the mutants. It can be used when the number of states in an implementation is equal to that of the specification. The idea is to analyze the structure of the specification and obtain an estimated number of faulty machines that can pass the given test suite. The number of conforming implementations can also be estimated 37 by taking the permutations of the state names. Fault coverage can then be calcu-lated as the number of faulty machines that cannot pass the test suite divided by the number of non-conforming implementations. A closely related issue is to decide the completeness of a test suite. A test suite is complete if its fault coverage is 100%, i.e., any fault in an implementa-tion can be exposed by the test suite. Vuong and Ko [101] proposed a method that generates a test suite guaranteed to be complete based on faulty machine gen-eration. We utilize the same idea of machine generation with further performance improvement and apply it to the evaluation of test sequence optimization techniques [108, 109]. Instead of generating all faulty implementations and then executing test suites against them, the idea of this approach is to only generate the machines that can pass the test suite but do not conform to the specification. This problem of machine generation is essentially a machine identification problem which intends to identify the internal structure of a machine by examining a finite external behavior. It is known to be NP-complete to determine if there is a minimal state machine that satisfies a given finite set of behavior [36, 37]. Therefore the generation of such a machine is also hard, i.e., no polynomial algorithms are likely. However, by using search optimization techniques borrowed from AI research, our algorithm can substantially reduce the computational complexity. Yao, Petrenko and Bochmann [106] also proposed a method that uses the same idea of machine identification but using state minimization techniques [57, 58] to generate a machine that can pass a given test suite. The techniques used there, i.e., generation of compatible coverings and verification of the closure property, essentially correspond to our domain reduc-tion and backtracking algorithms. However, the way that we formulate the problem allows further potential in improving the efficiency of the algorithm, namely more 38 heuristics or better search techniques can be developed. Another work of more practical nature is the one reported by Groz, Charles and Renevot [41], where the authors developed a practical tool that evaluates the coverage of a test suite in terms of transition coverage based on the Extended Finite State Machine model. 2.3.2 Testing of Communicating FSMs Most work in protocol testing focuses on testing single FSMs, such as the traditional W-method [19], DS method [39], UIO method [85], UIOv method [99], and a number of other methods (e.g., [32, 74, 105, 76, 67]) that were developed particularly in the context of protocol testing. These methods are sufficient in dealing with protocol entities that have a monolithic structure. However, many practical protocols are better specified in a structured way with cooperating components. Testing of such composite systems is a challenge since there are internal transitions that are neither observable nor controllable, and trying to covering all possible transitions would cause the state explosion problem. The P S P A C E hardness in generating test sequences covering a state or a transition was proved in [61]. Since deterministically covering all transitions is out of question in practice, probabilistic testing [20] was proposed to cover the more probable part of a C F S M , with the probability determined in advance base on the tester's knowledge. This approach requires prior knowledge of how probable a transition may happen and is not practical in many cases. Random walk is therefore proposed to achieve coverage of all transitions in each component machine in an adaptive way. Pure random walk would not work well since it tends to produce very long test sequences and there is no knowledge as to when all transitions would be covered. Guided random walk [61] and weighted random walk [56] are proposed to deal with it. Guided random walk 39 tries to choose untested transitions when a decision is needed in selecting the next test step. However, as pointed in [56] this simple mechanism degenerates quickly into pure random walk since after many transitions have been selected, the mechanism amounts to a pure random selection. Weighted random walk remedies this situation by using weight as a selection criterion when choosing a test step. Weight is calculated from the specification and measures the likelihood that a transition may lead to more untested transitions. When choosing a test step, the one with the highest weight among untested or tested transitions is chosen. This approach was shown to be more effective than pure and guided random walk [56]. While the above test methods aim at testing the C F S M system as a whole, there are methods that focus on testing an individual module within the system [79, 77, 53, 112]. When testing this module, all other modules are assumed to be correct, which form a test context for the module under test (MUT). Testing of the whole system can be done incrementally. Since the targeted module can be viewed as embedded in the composite system, this kind of testing is also referred to as embed-ded testing or testing in context, accommodating both the OSI embedded protocol testing and embedded module testing in hardware and distributed computing. Petrenko et al's work proposes the idea of generating an embedded equivalence of the M U T , which represents the M U T behavior that can be observed and controlled by the tester through the test context. Test suites can then be generated based on the equivalence module and the problem is reduced to single F S M testing. The work in [53] uses the general idea of F S M composition and keeps track of the M U T ' s internal transitions covered by external transitions. Test suites can be generated based on a test purpose specifying the transitions to be tested. In [112], we proposed an 40 approach based on coverage analysis. A n initial test sequence can be generated by random walk or composition that targets on all or some transitions in the M U T . This initial sequence is analyzed for its fault coverage. Additional test cases are then generated to increase the fault coverage to satisfy a certain coverage requirement such as limited by testing cost. 2.3.3 Metric based behavior coverage measure Contrary to the fault coverage, the behavior coverage endeavors to cover the behav-ior of a protocol without worrying about fault models. The philosophy here is that once the behavior is covered, the protocol system that passes the testing will work. That is, faults should have a good chance to be detected by behavior tests, thereby our confidence in the correctness of the implementation is increased. The fault de-tection efficiency analysis done for the transition tour method in [72] supports this philosophy. A n advantage of targeting on behavior coverage is that it is often less de-manding than fault based methods, which typically have exponential length of test sequences (e.g. the W method [19]) and may be fairly difficult to generate (e.g. NP-completeness in the CSP approach [101], P S P A C E hardness in UIO [85] deriva-tion [105], or unsolvability in determining mutant equivalence for general mutation testing [12, 27]). Among behavior coverage methods, the metric based method [100, 22] is novel and theoretically significant in that it provides a way to systematically ap-proximate the infinite behavior of a protocol by a finite test suite. In their approach, a metric based test selection and coverage analysis method was proposed, with the purpose of generating test cases that cover the specification in a "convergent" man-41 ner. The control behavior space of a protocol is considered as composed of execution sequences which represent the interaction between the protocol system and its en-vironment. A n execution sequence can be concisely represented as a sequence of (a,p), where a is an event and p the recursion depth of a. This is essentially a more compact notation for a trace. This behavior space is then turned into a metric space by imposing a metric among the execution sequences. Testing comes into play by assigning the metric a meaning of testing, leading to the concept of test-ing distance. The most important factor in the testing distance is the inclusion of recursion depth, which was considered as a major difference than other metric characterization of concurrency such as that in [38]. In such a metric space, with appropriate definition of the testing distance, the property of compactness can be proved, which provides a basis of test selection in such a way that the series of test suites resulted from the selection can converge to the original specification in the limit. Thus, we have a way to achieve coverage of the specification with an arbitrary degree of precision limited only by the test cost. This establishes a conformance relation between the implementation that passes the test suites and its specification. Note that this conformance relation is actually an extension relation in the sense that the implementation may contain more traces than specified in the specification. The testing efforts in trying to cover the traces belong to the realm of behavior coverage testing. Test selection in the metric based approach is essentially a pseudo-random testing guided by testing distance and test suite density. The effectiveness of the approach is backed up by research in software testing that showed random testing can be cost effective for many programs, and some subtle errors can be discovered without much effort [28]. The trade-off, however, is that the length of the test cases 42 may be quite long in comparison with fault based methods, probably because it may take many test cases to hit a particular fault. With today's powerful computers, this trade-off is becoming more acceptable than ever before, since the cost in generating fault targeting test cases may greatly outweigh the cost of running a longer test suite, which can be done unattended during off-work hours with much less cost. The problem with this method is that it can only handle a data-less protocol modeled as LTS or hierarchical LTS. In practice protocols, especially application ori-ented ones, are often extended with data storage. Data extension may dramatically increase the number of states in a system, and therefore makes the LTS (and FSM) based methods generally infeasible (although they are certainly useful in analyzing a protocol at a higher level of abstraction, e.g., when data are abstracted away, and useful in handling well structured protocols). There was also no complexity analysis on the length of such test suites with respect to test suite density. These issues will be dealt with in this thesis with the introduction of a generalized metric space. 43 Chapter 3 Coverage measure for single machine testing This chapter presents our results on a coverage measure for a single protocol entity modeled as a finite state machine. We describe the model, define the coverage measure, and then give algorithms that calculate the measure. A tool is built and real life protocols are used to demonstrate and test the approach. We further study the issue of incremental test suite generation and fault localization based on the measure. We close the chapter by using the coverage measure to evaluate various test sequence optimization techniques regarding their effect on the fault coverage. 3.1 Coverage measure In general, a measurement involves the association of an object and a number in such a way that certain observed relationships are maintained [83, 104]. This applies to a protocol testing coverage measure as well. In a protocol testing coverage measure, we are given a test suite T , and a 44 specification M 5 . Denote a coverage measure as C(Ms,T), and all possible test suites as TS, T 6 TS. The measure must be consistent with our observations that if a test suite is better than another one in terms of fault detecting capability or confidence in the tested protocol implementation, the coverage measure for the first one must be greater than the second. In other words, if we define a binary relationship is-better.than between two test suites T\, T2 e TS, the coverage measure must be assigned in such a way that for all T\,T2 € TS, isJbetter.than(Ti,T2) C(Ms,Ti) > C(MS,T2). To define a fault coverage measure, a fault model is necessary to limit the number of all possible implementations of a specification, since otherwise the cover-age would always be zero as the number of faulty implementations may be infinite. As pointed out in [12], there exist programming systems in which for any program S and finite test suite, there exists a function that agrees with S on the test inputs but disagrees elsewhere. FSM is such a programming system as widely identified. Therefore a fault model is needed to make a finite test suite relatively adequate (see Definition 2.4), or complete. We choose in our study the least restricted fault model, where the number of states in any implementation Mi is up-bounded and no less than the number of states in the specification machine Ms (assuming Ms is minimized). Besides, the input alphabet of Mi must be the same as M s . In this fault model, various combinations of output or transfer faults need not be treated specially. Using the concept of V-equivalence, we define the following terminology in the context of testing with the above fault model assumptions. Definition 3.1 (T-conforming) Let T be a test suite, Ms a specification ma-45 chine. An implementation machine Mi is said to be T-conforming to Ms iff Mi =T Ms. Definition 3.2 (T-indistinguishability) Let T be a test suite and Ms be a spec-ification machine. An implementation machine Mi is said to be T-indistinguishable from Ms if Mi =T MS and Mi -iconf Ms-Denote the set of all machines that conform to Ms as S C M (S-conforming machines), the set of all T-conforming machines as T C M , and the set of all T -indistinguishable machines as T I M , it can be seen that T C M D S C M and T I M = T C M \ S C M . T C M D S C M holds because all S-conforming machines must be T-conforming for any test suite T . T I M is the complement of the set S C M with respect to the set T C M . Figure 3.1 depicts this relationship. The shaded area is the set T I M . T I M represents the machines that do not conform to the specification but cannot be distinguished (detected) by the test suite. Therefore it measure the inefficiency of the test suite. The coverage, or the goodness, of the test suite can then be defined as the inverse of the size of T I M . Definition 3.3 (Coverage measure) Let KSCM = \SCM\, KTCM = \TCM\, and n be the upper bound of states in any Mi, the fault coverage of a test suite T is defined as: ' 0 ifT = <f>, Cov(Ms,T,n) = ' l KTCM—KSCM+1 otherwise. 46 All n-state FSMs SCM: Specification conforming machines TCM: T-conforming machines TIM: T-indistinguishable machines (TIM = TCM - SCM) Figure 3.1: Machines with respect to a specification and test suite The "1" in the denominator is necessary since it is possible that KTCM = KSCM which should be interpreted as complete coverage instead of infinite coverage, which does not make much mathematical sense. The is-better-than relation holds, since a test suite is considered better (or more effective) than another one if it can detect more faults, which means a smaller KTCM — KSCM- The coverage measure is also monotonic in that if T\ C T2, the coverage of T2 is no worse than that of T\. This consists with our observation that a test suite must detect no less faults than part of it. We therefore reach the following theorem: Theorem 3.1 The coverage measure Cov(Ms,T,n) satisfies the following proper-ties: 1. 0 < Cov(Ms,T,n) < 1. In particular, Cov(Ms,T,n) = 1 if KTCM = KSCM, i.e. T is complete. 2. IfTi C T2, then Cov(Ms,Tx,n) < Cov(Ms,T2,n). 47 Our coverage measure is different than the one used in the simulation ap-proach [90] and the structural analysis approach [107] in that we only calculate the number of TIMs of the specification. This is made possible by the fact that for a given n and Ms, the number of all possible implementations is a constant. The measure is thus a relative measure in that it is not an absolute measurement of the percentage of detectable faulty machines; rather it measures the relative fault detecting ability of test suites for a particular specification. We consider this as adequate since the quality of a test suite is only meaningful when compared with other test suites for the same specification1. 3.2 Coverage measure calculation To compute Cov(Ms,T,n), we need to: • calculate KTCM, i-e., to identify the number of machines that accept the test suite, and • calculate KSCM, to determine how many of these T-conforming machines actually conform to the specification. When computing KTCM, we use a constructive approach that builds all T C M s . This is necessary for further analysis of the test suite when there are non-conforming T C M s . We construct T C M s as complete deterministic machines (DF-SMs). The specification F S M can be either a complete or a partial D F S M , or a lrThe comparison of test suites for all protocols in general can be made between test generation methods regardless of a particular test suite. For example, the W method is better than the transition tour method in the sense that for any specification, test suite generated by the W method can always detect more faults than that by the transition tour. 48 non-deterministic F S M (NDFSM). The difference for our measure lies only in the computation of SCMs using appropriate conformance relations. 3.2.1 Calculation of KTCM The calculation of our coverage measure is a constructive approach. In comparison with the structural analysis method, we can obtain an accurate coverage value by explicitly generating all T-indistinguishable machines. The following advantages are identified: 1. The measure is both accurate and general. Accurate because the exact number of faulty machines can be identified, and general because it does not depend on detailed fault classes and all their possible combinations. 2. We can extend the method to generate a better test suite by adding new test cases that distinguish some or all T-indistinguishable machines. 3. With all T-indistinguishable machines explicitly enumerated, investigation of the reason why a test suite fails to be complete is made easier. This helps improve the test generation method. 4. When an implementation fails a test suite, fault diagnosis can be facilitated by constructing all possible faulty machines in the way same as the construction of all T-indistinguishable machines. A test suite T is a set of test cases, each starting from a reset. T is linear if it consists of only one test case; otherwise T is a tree with each test case being a subtree joined at a common root. As we only generate a deterministic tree, labels with the same input are merged. This eventually produces a so-called test tree [19]. 49 a/0 (UIO for each state: 0:a/l; 1: a/0 a/1; 2: b/1 a/1) ri/- a/1 a/0 a/1 ri/- a/1 b/1 a/0 a/0 a/1 ri/- b/1 b/1 a/1 ri/- a/1 b/1 b/1 a/1 UIO Test Sequence: Figure 3.2: Test tree corresponding to the UIO test sequence Figure 3.2 shows a sample F S M , its UIO test sequence (see [85] for a description of the UIO method), and the corresponding test tree. Construction of T-conforming machines can be considered as a process of "collapsing" the test tree back into one or more FSMs. Now we assign each node in the test tree a variable vi, with i numbered ac-cording to the node's breadth-first traversal order in the tree (see Figure 3.2). Where there is no ambiguity, we shall use the term node and variable interchangeably. The number of variables L, excluding vo, can be determined by a breadth-first traversal of the tree. For example, in Figure 3.2, L = 12. Initially, each variable can represent any state. Suppose the specification machine Ms has n states: Q = {qo, q\,qn-i}, then the domain of each variable is Q. Variable vo is always assigned to the root qo- A valuation of all variables such that their connections as constrained by the test tree form an F S M is called a solution for the variables. Such a solution is a T-conforming machine. Finding a solution is a search process that aims at instantiating variables with values in their domains when maintaining the consistency of the values, i.e., their 50 connections (transitions) are constrained by the test tree and they form a partial FSM. The simplest approach to this problem is to search the whole domain of all variables in some order and progressively assign consistent values to the variables, using the traditional search algorithm shown in Figure 3.3 [25]. It consists of two recursive procedures, Forward and Go-back. The first extends a current partial assignment if possible and the second handles dead-end situations. The upper bound of the computational complexity of this algorithm is 0(nL) and is out of question for any practical size protocols. However, deterministic FSMs have some properties that allow pruning of the search space. Recall in the general definition of FSM (Definition 2.5), an FSM is deterministic if there is only one transition for any input. Let F = {Q,X,Y,qo,S, A) be an FSM. This determinism can be formally defined as: (CI) Vqi,qj,qk E Q Vx € X : 8(qi,x) = qj A S(qi,x) = qk q5 = qk. An immediate corollary is that if two states produce different outputs for the same input, then the two states must be different, i.e. (C2) Vqi,qj e Q Vx € I : X(qi,x) X(qj,x) ^ qi ^ qj. Extending this to a sequence of input, we can conclude that if two states produce different output sequences under the same input sequence, then the two states must be different (i.e., V-distinguishable). Let X* denote the set of all finite-length input sequences, then (C3) Vqi,qj S Q Ver G X* : \(qi,o) ^ X(qj,a) =4> qt ^ qj. Using these properties, we can use the following techniques to reduce the computational complexity of our algorithm. 51 Algorithm 3.1 (Backtracking search) ( u i , V i ) : the list of variables; Ci: the list of candidate values for Vi. Forward (v\v*) { 1. if i = n then exit with the current assignment. 2. Ci+i <— Compute-candidates (vi, . . . ,«j , .Ut+i) / 3. if Ci+i is noi empty then { ^ . Uj+i «- yirsi element in Cj+i; 5. remove Vi+i from Cj+i; £. Forward (vi,Vi, vi+i); 7- } 8. else Go-back (v\,...,Vi); } Go-back (v\, ...,Vi) { 1. if i = 0 then exit. No solution exists. 2. if Ci is not empty then { 3. Vi «— first in Ci; 4- remove Vi from Ci; 5. Forward (vi,..., Vi); 6. } 7. else Go-back (vi, ...,Vi-i); } Figure 3.3: Simple backtracking algorithi 52 (1) Preprocessing: Although the domain of each variable is Q, the deter-ministic property will often restrict the values that a variable can assume. For example, according to C2, a variable cannot take on the value of a previous variable unless they are equal. In the extreme case, each variable may only have one value, indicating a complete fault coverage of the test suite. We reduce the domains of the variables in the breadth-first order. For each variable vt, we can obtain a set of variables, called unequal variables of Vi, whose indices are smaller than i and whose values are different from that of Vi. Variables that can only have one value constitute the unique set. Initially, the unique set contains VQ only. The uniqueness of a variable vi can be determined by examining its set of unequal variables. If this set contains the current unique set, then Vi must itself be a uniquely determined variable and is added to the unique set. To prevent isomorphic solutions2, the unique state qj assigned to Vi is chosen such that j is the smallest index not yet assigned. For example, if Vi is the first one that differs from vo, then it is assigned q\. The first variable that is distinct from VQ and Vi is then assigned the next unassigned state, q2. A variable that is not in the unique set but has some unique states in its set of unequal variables can have these unique states removed from its domain. This is because it is not possible for the variable to assume any of these values. This procedure is performed until all variables have been processed. The results are a reduced domain and a set of unequal variables for each variable. The preprocessing phase often prunes the search space significantly and saves considerable time in the subsequent searches. Furthermore, for any variable Vj which is not uniquely determined, its set of unequal variables can help to reduce the search isomorphic solutions differ only in the naming of the states. There is no need to generate them as they do not contribute to the coverage measure. 53 space dynamically, since it will not be necessary to assign Vj a value which has already been assigned to any of its unequal variables. (2) Backjumping: During searching, when a variable cannot be assigned any value which is consistent with the previous assignments (a dead-end situation), we can jump back to the variable which causes the inconsistency rather than backtrack-ing one step at a time as is usually done. This idea is widely used in solving search problems [25]. The point is to go back to the source of failure as far as possible. In our problem, when a variable is instantiated, it may be forced to take a value in one of two ways. First, it may only take a single value if its domain size is one. Second, the assignment of a previous variable which has the same input symbol may force it to assume the same value in order to be consistent with the properties of a deterministic FSM. Such value-forced variables cannot be the source of failures, so when a dead-end is encountered, they need not be reconsidered in selecting can-didates. This situation will occur very frequently when the test sequence contains many identical transitions. The algorithms for preprocessing and backjumping search are given in Figure 3.4. In Step 1, the set of unequal variables for each variable is generated. The if statement is executed L(L — l)/2 times. The evaluation of the condition Vi ^ Vj is based on property C3. Since input sequences starting from a node constitute a subtree rooted at that node, the evaluation can be performed by comparing two subtrees rooted at Vi and Vj respectively. The comparison can be done by means of a breadth-first search algorithm for the subtree. When comparing two nodes, property C2 is used. When a pair of distinct nodes is found, the two subtrees are distinct (C3). However, when subtrees are incomplete, the node with an absent 54 Algorithm 3.2 (Domain reduction of node variables) Input: Node variables Vi,i = 1,..,L Output: Reduced domain Di for each Vi and its unequal variables NEQi. Step 1: Generate unequal variables: Initially, the set of unequal variables for each Vi, NEQi — 0-for every Wj (1 < i < L) do for every Vj with j < i do if (vi ^ VJ) then add Vj to NEQi. Step 2: Reduce domains of variables: Initially, the set of uniquely determined variables U = {vo}, state set Q = {qi,qn-i}, and the domain for Vi(i = 1 , L ) is Di = QU{q0}. for every Vi (1 < i < L) do if (U C NEQi) then { add Vi to U; Di 4— {qk}, k = the smallest subscript in Q ; Q+-Q- {Qk}; for all Vj E NEQi do Dj <- Dj — {qk}; } else for all Vj E NEQi do if Vj E U then Di 4- Di - DJ; Figure 3.4: Domain reduction algorithm 55 edge is not considered distinct from its corresponding node where the edge is present. For example, in Figure 3.2, although v2 has no edge corresponding to a, we cannot conclude v2 must be different from VQ. Similarly, v$ may possibly be equal to v2. The time complexity of tree comparison is at most 0(L). Hence, the complexity of Step 1 is 0{L3). The domains are reduced in Step 2 using the NEQ sets. If NEQ; contains the , current uniquely determined variables, vi itself becomes a member of U. For each member Vj of U, the domains of i>j's NEQ variables can be reduced by removing Vj's corresponding value. The idea is that if a variable is not equal to a uniquely deter-mined variable, it cannot assume the unique value of that variable. The complexity of this step is 0(L2). Thus, the overall complexity of Algorithm 3.2 is 0(L3). Note that the test tree has to be constructed from the test sequence before using this algorithm. The procedure Compute-candidate in line 1 selects a consistent value for vt from its domain (we shall say that Vi is instantiated). The reduced domain and the set NEQj both help reduce the number of candidates. During the instantiation process, it builds up a partial solution FSM with the values of variables up to Vi, one by one. To determine a consistent value of Vi, let vv be v^s parent node in the test tree, and the I/O label from vp to Vi be x/y. Suppose vp has the value qp which is a state in the partial FSM. If qp has no outgoing transition labeled x/y, then we get a value for Vi which is the next state (say qt) in its domain, and a new transition from qp to qt is added to the partial FSM. Otherwise, Vi is forced to be 6(qp,i) in the FSM, because for a label x/y from a state qp we can have at most one transition (refer to C l ) . 56 Algorithm 3.3 (Backjumping search) Input: Node variables with reduced domains and the specification Output: The set of indistinguishable FSMs Initially, the index of variables i = 1. A stack is used to store intermediate steps. 1. Ci <— Compute-candidate (vi); 2. if a = NONE then { 3. /* dead-end encountered */ 4- i <— popstack; 5. if stack is empty then 6. exit with no more solutions; 7. goto 1; 8. } 9. else { 10. if Cj is not a forced candidate then 11. pushstackfi); 12. i 4-i + l; 13. if i = L + 1 then { 14- /* a solution F is found */. 15. minimize F and record it; 16: if F is equivalent with an existing solution then 17. discard F; 18. else 19. check F's conformance with the specification; 20. i <— popstack; 21. } 22. goto 1; /* go on searching */ 23. } Figure 3.5: Backjumping search algorithm 57 The partial F S M is constructed incrementally until all variables are assigned consistent values, at which time the F S M becomes a final solution. To avoid iso-morphic solutions, when instantiating Vi, only one value out of a set of equivalent candidates is selected. The candidates are equivalent in the sense that they repre-sent equivalent states in the current partial F S M . If one of the equivalent candidates fails, the others will fail too. This fact is used to reduce the domains to be searched dynamically. Compute-candidate returns N O N E when no consistent value of Vi can be found. This is the dead-end situation so backjumping is invoked. Since a forced variable cannot be the source of a failure as mentioned before, line 11 pushes a variable that was not forced a value onto the stack for subsequent backtracking. In line 13, i = L + 1 means all variables have been successfully instantiated, and a solution F is found. Line 16 checks if F is equivalent with any existing solution machine after minimization. The minimization is necessary since a solution may not be reduced. F will be discarded if it is equivalent with any machines that have been generated. Otherwise, F is checked for conformance with the specification (line 19), i.e., to check if the solution is a member of S C M . A non-conforming solution represents a T-indistinguishable machine. 3.2.2 Calculation of KSCM So we need to calculate K$CM to complete our coverage measure calculation. As mentioned in Section 2.2.2, equivalence, quasi-equivalence, and reduction relations are used as our conformance relation conf(Definition 2.11), and KSCM = \{M\M e T C M A M c o n f 5}|. The quasi-equivalence relation allows us to consider an implementation as an extension of the specification machine in the sense that the implementation contains 58 the specification. This is reasonable in the following cases: 1. When an implementations has more states than its specification. This is typi-cal in implementations that offer more than required such as additional func-tionality in exception handling. Such an implementation must be considered conforming; 2. When the specification machine is partial. In this case, we allow the imple-mentation to choose any transition to implement at its own discretion, i.e., we use the "undefined by default" semantics for unspecified transitions. Quasi-equivalence is sometimes called a, containment relation, to reflect the1 asymmetricalness of the relation. A machine Mi contains machine Ms iff M / >z Ms'. This relation applies to both complete and partial FSMs. When applied to complete FSMs, the relation holds when M / has no less states than Ms- For partial FSMs, M j contains Ms when M / exhibits the same behavior for the input sequences defined in Ms- Note that if we consider unspecified transitions in a partial F S M as "implicitly specified" or "prohibited", it amounts to completing the machine3, and therefore strong conformance relation is appropriate. The standard algorithm for checking strong equivalence [3] can be slightly modified to check containment (Figure 3.6). Here we assume that Mi and Ms have the same input output alphabet, since in conformance testing, we only test those inputs and outputs specified in the specification (additional I /O behavior in an implementation can be tested in, say, robustness testing). In Figure 3.6, operation UNION(Ai , A2, A\) (line 10) replaces sets A\ and A2 in C O L L E C T I O N by Ax = Ax l)A2; FIND(c/) (line 8) gives the set of which s is 3In the single machine testing model, we allow the tester to send any event to the IUT which must respond to it even if it is considered "prohibited". 59 Algorithm 3.4 (Conformance checking for DFSM) Input: Two DFSMs Mk = (Qk,X,Y,qk,Sk,Xk), k E {I,S}. Output: Mi conforms to M$ or not. 1. LIST = {(qi,qS)}; COLLECTION = cp; 2. for each q in Qj U Qs do add {q} to COLLECTION; 3. while there is a pair («7i,<72) on LIST do { 4- for all x E X do { 5. if 5s{q2, is defined then 6. if \r(qi,x) = Xs{q2,x) then { 7. LIST 4- LIST —{(qi,qi)}; 8. Let Ai <- FIND{qi),A2 «- FIND{q2); 9. if Ai ^ A2 then { 10. UNION(A\, A 2 , Ai) ; 11. LIST <- LIST U{(SI(q1,x),Ss(q2,x))}; 12. } 13. } 14- else Mi does not conform to Ms; exit. 15. } 16. } 17. Mi conforms to Ms-Figure 3.6: Conformance checking for deterministic specs 60 Algorithm 3.5 (Conformance checking for NDFSM) Input: DFSM Mj, NDFSM Ms. Output: Mi conforms to Ms or not. 1. LIST = {(qi,qS)}; COLLECTION = <f>; 2. for each q inQiUQs do add {q} to COLLECTION; 3. while there is a pair (91,92) on LIST do { 4- for all x G X do { 5. NSTATS 4- 5s{q2, x); /* set of next states for q2 */ 6. if NSTATS ^ <p then 7. if 3n G NSTATS : 6s(q2,x) = n A A/(gi,a;) = \s(q2,x) then { 8. LIST <- LIST - (qi,q2); 9. Let A i 4- FIND(qi), A2 4- FIND{q2); 10. i f A i ^ A 2 t h e n { 11. UNION(Ai,A2,Ai); 12. LIST 4- LIST U (Si(qi,x), n); 18. Mi conforms to Ms-Figure 3.7: Conformance checking for non-deterministic specs a member. These are two basic operations on sets. Algorithm 3.4 can be adapted to check the reduction relation when the spec-ification is an NDFSM (Figure 3.7). The difference lies only in the comparison of output sequences. Whereas in DFSM the output sequence for an input sequence is uniquely defined, in NDFSM it can be a set of sequences. The comparison thus has to be done as a set membership checking for the reduction relation. Using Algorithms 3.4 and 3.5 to check the machines in set T C M for their conformance with the specification, the set SCM can be computed and its size is 13. 14. 15. 16. } 17. } 61 KSCM- This completes our calculation of the coverage measure. 3.2.3 An i l lus trat ive example We shall use the F S M in Figure 3.2 to illustrate the above algorithms. Initially, Do = {go}, D{ = {qo,qi,q2} for i = 1 , 1 2 . From the tree, it can be seen that v\ must be different from VQ as their outputs to a are different. At this point, only vo is in the unique set U, so v\ is also a uniquely determined variable. v\ is then assigned q\, the next value in the state set. Next, v2 is found to be distinct from v\ because of their different outputs for 6a. Therefore v\S value gi is removed from v2's domain. After all variables have been processed, their domains are found to be: D\ = {qi},D2 = {qo,q2},D3 = {q0},D4 = {g2}, D5 = {qo},D6 = {qo,qi,q2},D7 = {qi},D8 = {q0}, A> = {90,91,92}, £>io = {go}, = {90,91,92},-D12 = {90,91,92}-Note that the domains for most nodes have reduced, some of which have only one candidate. Those domains that were not reducible are all for leaf nodes since they have no outgoing edges (we'll see that this does not affect the search process). Now Algorithm 3.3 is used to search for solutions. For the first five variables, only v2 has more than one choice. We first choose 90, which is consistent with v\ = 9 1 . The remaining variables are forced to take the values 91, 91, 90, 91, 90, 91, and 91 respectively. Thus, we obtain our first solution: vo - 90, vi=qi,v2 = 90, v3 = 90, vA = q2, v5 = g 0, w6 = 9 i , V7 = qi,vs = qo,v9 = quvw = 9 o,«n = 9 i , « i 2 = 9 i -Since all variables after v2 were forced, the algorithm goes directly back to v2 to find the next solution. The next candidate for v2 is 92, which is also consistent with v\ = 91 . The other variables are again forced to the same values, producing another 62 solution: vo = qo,vi = qi,v2 = q2,v$ = qo,v4 = q2,v5 = q0,v6 = <?i, V7 = qi,v8 = q0,v9 = qi,vw = qo,vn = <?1,^12 = gi-lt can be seen that the variables cannot take on any other value, so the algorithm terminates with two solutions. Figure 3.8 shows the two corresponding FSMs, with the first one an indistinguishable F S M , and the second one conforming to the specification, i.e., KTCM = 2 and KSCM — 1- Therefore the (relative) coverage of the test sequence is Cov(Ms,T,S) = l - — = 0.5. i^TCM — i^SCM + 1 The two solutions are both obtained backtrack-free, which means only O(L) time is needed to get a solution. This is the best result we can hope for. We also observed that although domains for the leaf nodes cannot be reduced, they are usually forced to some values. For example, ^6, ug, vn, and v\2 were all forced variables. (a) Solution 1: T-indistinguishable FSM1 (b) Solution 2: T-indistinguishable FSM2 Figure 3.8: The two solutions for the UIO test sequence given in Figure 4 63 3.3 Applying the measure to real life protocols The example in the above section was too small to show the effectiveness of the method to real life protocols. Three real life protocols, the ISDN Basic Rate Interface (BRI) D-channel signaling protocol [2], T C P protocol connection management [30], and the NBS Transport Protocol class 4 (NBS TP4) [90], were chosen to test our approach. The sizes of the protocol machines are typical for single module protocol entities, where abstraction may be needed to stress on major functionality of the protocols. We have developed a tool, called C O V , which implements our approach, including the algorithms presented in the prior section. C O V was written in C and tested on Solaris, OSF/1 and Linux. It accepts as input a test suite T, the specification machine Ms, and the maximum number of states in any Mj. The output is all T-indistinguishable M/'s with respect to Ms, i.e., the set T C M \ S C M . The coverage measure is then calculated according to Definition 3.3. 3.3.1 I S D N B R I protoco l The Integrated Service Digital Network (ISDN) was proposed in 1984 to provide integrated voice and digital services over a fully digital, circuit-switched telephone system. One of the ISDN interface is the basic rate interface (BRI) which has one D-channel and two B-channels. The D-channel signaling protocol is defined in C C I T T Recommendation Q.931 [14]. It is located at the network layer as a user-network interface, specifying the procedures for establishing, maintaining, and clearing basic circuit-switched voice connections. The protocol is defined between the user and network interfaces for incoming and outgoing calls. We only consider the network side of the Q.931 BRI for basic voice services at the originating end. The state 64 N10 , ACTIVE 1. UM?setup_bad/Ulj 2. UI_1?rel/UI_1!relcoir 3. UM?setupAJL1lseti 4,10. UI_1?rel/UM?reli 5. UM'info/UMIinfo 6. UM?info_last/UI_1!i 7.13. T302?tlmeout/UI_ 8.14. Ul_1?info_bad/Ul. 9. UI_1?discAJMIrel 11. UI_1?info/null 12. UI_1?infoJast/UI_1 15. UM?discAJMlrel 16. U1_1?rel/UI_1lrelcoii 17. NI_2?netalert/UI_1fc 18. Ul_1 ?disc/UI_1 !rel 19. Ul_1?rel/UI_1lre1coi 20. NL2?netconn/UI_1! 21. NI_2?netclearAJI_1! 22. UI_1?dlscAJI_1lrel 23. UI_17rel/UI_1lrelcoi 24. UL1?connack/nul1 25. NI_2?netclear/UI_1l 26. UI_1?disc/UI_1lrel 27. UM?relflJI_1lrelcoi 28. UL1?dlscrtJL1!rel 29. T3057timeoutrtJL1! 30. T308?timeOut/UI_1! 31. UI_1?disc/null Figure 3.9: ISDN BRI network layer protocol (network side at the originating side) diagram of this protocol is shown in Figure 3.9 ([2]). The notation used in Figure 3.9 is as follows. The transition label A?mi/B\rrij is interpreted as receiving the input message mi from F S M A , and sending the out-put message rrij to F S M B. Table 3.1 lists the UIO sequences for each state. The whole set of test suite is listed in Appendix A which was generated by a tool we developed. There are a total of 8 states, 14 inputs, 12 outputs, and 425 test steps (transitions). The machine was completed with the completeness assumption: for unspecified transitions, a self-loop transition is added to the state with a null output. This is commonly used in protocol testing, since a protocol implementation must choose a way to handle inputs that are not specified in the specification. This can 65 be either the above completeness assumption, weak conformance based on quasi-equivalence, or prohibition (see Section 2.2.2). Table 3.1: UIO Sequences for BRI State U I O Sequence NO UI_1 ?setup_bad/UI_l Irelcom NI UI_l?info/UI_l!info N2 UI_l?info/null N3 NI_2?netalert/UI_1 lalert N4 NI_2?netconn/UI_l!cpnn N10 UI_1 ?connack / null N12 T305!timeout/ULl!rel N19 UI.l?disc/null The test suite was analyzed using C O V , and in less than a second, a unique solution was found backtrack-free, i.e., KTCM = KSCM = 1- The coverage of the test suite is therefore 1. This confirms that the test suite is complete, although in general UIO method does not give a complete test suite. ;, 3.3.2 T C P connection management protocol T C P (Transmission Control Protocol) [30] is a connection oriented Internet trans-port layer protocol. It provides a reliable end-to-end byte stream over an unreliable internetwork. Since the underlying network is assumed to be unreliable, connection establishment becomes a tricky task as the network may lose, store, and duplicate packets. A sophisticated three-way handshake is therefore used for establishing T C P connections. Releasing a connection is also tricky because of the so-called two-army problem (see Section 6.2.3 of [92]). There is no perfect solution to this problem; however, in practice, using timers usually suffices as is done in T C P . We take the T C P connection management protocol as our example. The 66 \ i data transfer part can be tested as a sub-module after the protocol gets into the "ESTABLISHED" state. This is actually a common "divide and conquer" rule in testing, i.e., testing hierarchically when the protocol admits, in order to control the complexity. The state transition diagram is shown in Figure 3.10. The messages C O N N E C T , L I S T E N , SEND, and C L O S E are user initiated while S Y N , FIN, A C K , and R S T are messages from or to the network. There are two timeout events, one for connection and one for disconnection. Transitions are labeled as Alvriij'Blrrij for receiving a message mi from A and sending mj to B. Here A can be "U" for user initiated messages, "N" for network messages, or a timer identifier for a timeout message. Table 3.2 gives the description of the protocol states. We choose to use the DS-method [39] to generate a strong conformance test suite. A distinguishing sequence for the F S M is: C O N N E C T S Y N _ A C K SEND FIN C L O S E FIN_ACK FIN T2_timeout C O N N E C T A C K C O N N E C T . The full test suite is given in Appendix B, with 1920 test steps, as generated by our tool. This test suite was fed to C O V and in about 3.5 seconds, a unique solution was generated, proving that the test suite was complete. 3.3.3 NBS TP4 protocol The NBS Transport Protocol is a protocol developed by the US National Bureau of Standards (now called National Institute of Science and Technology) [89, 90], of which Class 4 is the most complex one of all the NBS protocol classes. This protocol is a predecessor of the ISO/OSI transport protocol and has been obsolete by and large. We use it in our study since it represents the order of complexity for most real life protocols. A subset of the protocol, with 15 states, 27 inputs and 26 outputs, is 67 Figure 3.10: T C P connection management F S M Table 3.2: T C P states and their descriptions State Description CLOSED No connection active or pending LISTEN Server is waiting for an incoming call SYN_RCVD A connection request has arrived; wait for ACK SYN.SENT The application has started to open a connection ESTABLISHED The normal data transfer state FIN.WAIT.l The application has said it is finished FIN.WAIT.2 The other side has agreed to release TIME.WAIT Wait for all packets to die off CLOSING Both sides have tried to close simultaneously CLOSE.WAIT The other side has initiated a release L A S T . A C K Wait for all packets to die off 68 chosen, which consists of the major functions of the protocol (excluding transitions for data transfer, expedited data, and close request service primitives). Figure 3.11 shows the F S M diagram for the protocol [90]. The F S M is completed with the completeness assumption in order to test strong conformance. A distinguishing sequence for the F S M is found to be: U_cr N_AK' NJ3R N_AK Ucq N_cc N_GR The test suite consists of 4131 test steps. Feeding the test suite to our tool C O V , running on a Sun Sparc Ultra-60 machine, it was able to produce a unique solution in about 22 seconds. Although we cannot draw a general conclusion from this result, we see it as a good sign that protocols of this size can be handled sufficiently with our approach. 3.4 More experiments In addition to the application of our approach to real life protocols, we have also performed more experiments on some FSMs found in the literature that are often used as sample machines, in order to see the performance of our algorithms empiri-cally. Our results show that the approach is promising in solving this hard problem. The actual complexity also tends to be dependent on test suite structure. In [24, 90], some examples were used for fault coverage evaluation using the Monte-Carlo simulation method. The W, DS and UIO methods were eval-uated in [90] with the conclusion that they all had the same full coverage for strong conformance test. Nevertheless, since the number of all possible machines is 1 5 1 0 ( « 5.7 • 10 1 1) for the sample machine M (FSM1 in Figure 3.12), and only 106 randomly generated machines were examined, the conclusion needs to be verified. 69 Figure 3.11: A subset of NBS Class 4 transport protocol 70 B/1 FSMl FSM2 FSMS Figure 3.12: Sample FSMs used in performance experiments With our tool, we were able to confirm that the three test sequences given in the paper do not have any T-indistinguishable solutions (see Table 3.3 for F S M 1) and thus have a 100% fault coverage4. The example in [24] (FSM2 in Figure 3.12) for UIO method also has a unique solution. A n encouraging observation is that all solutions were obtained backtrack-free. To further evaluate our tool, we studied the W method with one extra state (denoted as W + 1 in Table 3.3), using the same sample F S M l . The original example for the DS method in [39] (FSM3 in Figure 3.12) was also studied for both the DS and UIO methods, assuming it is resettable. The results for the three real protocols, i.e., the ISDN BRI network layer protocol, T C P connection management protocol, and a subset of the NBS TP4 protocol are also included. The fault coverage values for these examples were all found to be 100%. Table 3.3 summarizes the results of our experiments. In the table, (n, m,p, L) is the number of states, inputs and outputs for the example, and the length of the test sequence, respectively, k is the number of T-indistinguishable solution machines. 4We note that although for the given example the UIO method does produce a complete test suite, later work [99, 66] discovered that UIO method in general does not produce complete test suites. 71 Table 3.3: Performance of C O V for some examples No. of No. of Example Method {n,m,p, L) k backjumpings forced cases Time (s) UIO (5,2,3,29) 0 (0, 0) (9, 9) 0.04 FSM1 DS (5,2,3,35) 0 (0, 0) (12, 12) 0.04 W (5,2,3,58) 0 (0, 0) (18, 18) 0.05 w + 1 (5,2,3,130) 0 (0, 60) (48, 558) 0.15 FSM2 UIO (7,4,4,111) 0 (0, 15) (38, 256) 0.13 FSM3 UIO (6,2,2,40) 0 (8, 59) (35, 203) 0.09 DS (6,2,2,62) 0 (0, 0) (25, 25) 0.07 ISDN BRI UIO (8,14,12,425) 0 (0, 0) (105, 105) 0.08 T C P DS (11,12,5,1920) 0 (1,8) (1461, 1575) 3.54 NBS TP4 DS (15,27,26,4131) 0 (105, 488) (2874, 2909) 22.86 The solutions for the examples we tried are all unique and conform to the original specification (KSCM = KTCM), which indicates a complete fault coverage. Two numbers are recorded in the column for "No. of Backjumps" and also the column for "No. of Forced Cases". The first one is the number when the first solution is found, and the second when the algorithm terminates. Forced cases occur when a variable is forced to take a value during instantiation. The larger the number of forced cases, the better the gain from backjumping. The number of backjumps gives an idea on savings from directly going back to the source of failure. The column "Time", obtained with the C-shell built-in command time on a Sun Sparc Ultra-60, is the average C P U seconds consumed by the tool in 10 runs, including input and output processing. The results showed that the strategy of preprocessing and backjumping is quite effective. Even a sizable real protocol like NBS TP4 can be handled efficiently. As seen from the T C P protocol experiment, we also observe that protocols are often amenable to hierarchical decomposition with clearly separate functional modules or phases such as connection establishment, data transfer, and connection release. This 72 decomposition allows reasonable sized finite state machines in each phase. Testing can then be proceeded phase by phase, leading to sub-problems that are within the capability of various tools including our own. 3.5 Incremental test suite generation When we test a communication protocol, we often want to achieve high fault cover-age whenever possible since communication reliability is often crucial in distributed computing. There are methods such as W, DS and UIOv methods that can guar-antee to produce a complete test suite, however the length of the test suite is often very long. For example, the upper bound of a preset distinguishing sequence for an n-state F S M is (n — l ) n n [59] 5. The total length of a test suite is 0(n2) longer since the machine needs to be brought to each state and each transition needs to be tested. When such a test suite is considered too long, one is left without knowing how to reduce the test suite to achieve a certain coverage. In contrast, our method lends itself to incremental test suite generation based on coverage requirement. Since we generate all T-indistinguishable machines (TIMs), we can choose to enhance a test suite by further distinguishing the TIMs. When more TIMs are distinguished by additional test cases, test coverage is increased. We stop adding more test cases when a certain test coverage is satisfied. The extreme case is when the coverage reaches 100% , i.e., when no more TIMs exist. In our coverage model, if a test suite is not complete, it follows that S C M ^ T C M , i.e., there are T-conforming machines that do not conform to the specification machine. If we can find I /O sequences that can differentiate some or all of those 5 A n adaptive distinguishing sequence can be shorter, though, with length at most n(n — l)/2 as reported in a recent work [62]. 73 machines from the specification, they can be added into the test suite. This new test suite must have better coverage since there are fewer T-conforming machines that do not conform to the specification. This leads to our approach based on the generation of distinguishing sequences. Generation of distinguishing sequences Suppose we have a set of T-indistinguishable machines (TIMs) for an F S M Ms and a test suite T. These TIMs all have the same input and output alphabet as Ms-The goal is to generate a distinguishing sequence A such that the output sequence of each T I M in response to A is different than that of Ms- This concept is similar to but different from the distinguishing sequence in the traditional finite-state machine theory [59, 34] in that the latter distinguishes among all states of a single machine. Distinguishing sequences are used to identify the unknown initial state of a machine. It may not exist for a machine, and it is PSPACE-complete to determine whether an F S M has a preset (i.e., the input sequence is fixed ahead of time) distinguishing sequence [62]. We extend this concept for two FSMs in the following way. Definition 3.4 (Distinguishing sequence) A distinguishing sequence for two FSMs Mi = {Qi,Xi,Yi, qio,Si,Xi) (i = \,2) is an input sequence Xd € X{ fl X£ such that the output sequences produced by the two machines from the initial state in response to Xd are different, i.e., \(qw,Xd) X(q20,Xd). In our case, since a T I M has the same input and output alphabet, i.e., X\ — X2 and Y\ =Y2, Xd is defined over X\. While a traditional distinguishing sequence may not exist even for a reduced F S M , our distinguishing sequence (DS) will always exist since the two machines in question (ie a T-indistinguishable machine and the specification machine) are known to be neither equivalent nor quasi-equivalent. 74 Our method for the generation of the DS is incremental. We pick up a ma-chine from the set of TIMs, find a DS that distinguishes it from Ms, and use this DS to distinguish some of the remaining TIMs. This will give us a new improved cover-age value. If this value satisfies the user requirement, the procedure is terminated. Otherwise we do the same for all remaining TIMs, excluding those already distin-guished by previous DSs. The procedure continues until user's coverage requirement is satisfied. To do this, first of all we need to generate a DS for a pair (Ms, TIMj). Since both Ms and TIMj are strongly connected and we know they are not equivalent, a breadth-first traversal of the machines guarantees to produce a distinguishing sequence, as shown in Algorithm 3.6 (Figure 3.13). The idea of the algorithm is to build a successor tree during the breadth-first traversal. The root of the tree is the pair of initial states of the two machines. The tree is expanded as follows. For each input applied to both machines, an edge labeled with input symbol and a new node labeled with pairs of states reached from the current node by the input are generated. A node in the tree becomes terminal whenever its labeled state pair has occurred before. The algorithm terminates when an input causes the two machines to produce a different output. At this point, a DS is found to be the input sequence from the root to the current node. This DS is of minimal length since no shorter sequence can distinguish the two machines. If we want to generate all possible DSs, we can simply change the termination criterion to there being no more new, expandable nodes. Consider an example in Figure 3.14. There are 10 solutions for the specifi-cation (a) with respect to the following test sequence: 75 Algorithm 3.6 (Generating DS for two FSMs) Input: Two FSMs Ms and MT. Output: A DS ( A ) for Ms and MT-1. VISITED = <f>; QUEUE = 4>; 2. en<iueue{QUEUE, {qs,qT, <P)); 3. while QUEUE is not empty do { 4. (qi,q2, A ) = dequeue{QUEUE); 5. VISITED 4- VISITED U'{(qi,q2)}; 6. for all x € X do { 7. if Ss{qx,x) is defined then 8. if A s ( 9 1 , x) = A T ( 9 2 , x) then { 9. if (91,92) € V7SiT£I>then continue; 10. A <— A o x; /* append x to A */ 11. enqueue(QUEUE, (Ss(qi,x),dT{q2,x),A)); 12. } 13. else { 14- A DS A is found; .Output A and exit. 15. } 16. } 17. } Figure 3.13: Generation of a DS for two FSMs 76 c/z c/z b/y a/y c/z c/z b/y a/y c/z a/y a/y c/z b/x a/y c/z c/z b/y a/y a/x c/z a/y b/y b/y a/y c/z c/z a/x c/z c/z c/x b/y a/y b/x a/y b/x c/x b/y a/y Of the 10 solutions, one is conforming (FSM3), and the rest are all T -indistinguishable. Take the specification and FSM6 as inputs for Algorithm 3.6. The successor tree for the two machines is shown in Figure 3.15. The tree is trun-cated when a node becomes terminal. The input sequence bba was found to be the minimal DS for the two machines. This DS can actually distinguish the specification from all remaining TIMs except FSM8, which implies a new coverage value of 0.5. If this is the coverage required by the user, we stop here. Otherwise, we can find a DS for the specification and FSM8, which is bbc. Therefore we obtain two additional test subsequences at this step: b/x b/y a/x, b/x b/y c/x Our tool C O V confirms that with these two additional subsequences, the entire test suite becomes complete. Suppose the two machines have m and n states respectively, then the number of state pairs is mn. This is an upper bound on the number of nodes in the successor tree since recurring nodes are eliminated. Therefore the depth of the successor tree cannot exceed mn because otherwise there would be recurring nodes on the path from the root to the deepest node. This leads to the following theorem: T h e o r e m 3.2 For two FSMs, MS = (Q, X, Y, q0, A, 6) and MT = {Q', X, Y, q'0, A', 6'), if MT does not conform to Ms, then there exists a distinguishing sequence whose length is no longer than \Q\ * \Q'\. 77 Figure 3.14: A specification F S M and its solution machines 78 (0,0) (0,0) (0,0) Figure 3.15: The successor tree for DS generation Note that this bound is not necessarily the least upper bound. In fact, since not all pairs of states are reachable, the minimal DS is often a lot shorter than mn. 3.6 Fault localization By fault localization we mean to locate a fault in a system that fails a test suite. It is also referred to as diagnosis of a faulty system. During this process, it is assumed that the implementation under test (IUT) remains a black box, and the diagnosis can only be done based on the IUT's erroneous behavior with respect to the test suite. The basic idea of applying our coverage measure to fault localization is to use a test suite and the (incorrect) responses from the IUT as the input to C O V . In this case, C O V simply constructs all T-conforming machines (TCMs) but does not worry about whether they conform to the specification. The task of fault localization is then to pinpoint which T C M represents the IUT machine. The difference of this T C M with the specification gives us the diagnosis on where the fault is located, such as a transition may have produced a wrong output or it has gone to a wrong next 79 (0,0) (1,2) state. To pinpoint the IUT from the set of T C M s , we need to find out an input sequence that distinguishes among all the T C M s . This is a generalization of our distinguishing sequence used in the previous section, hence we call it a general distinguishing sequence (GDS). GDS is different from DS, which distinguishes each T I M with the specification. Depending on whether the GDS is fixed prior to fault localization, preset or adaptive GDS can be generated to pinpoint the faulty IUT. We define a general distinguishing sequence for a set of FSMs, Mj = (Qi, Xi, Yi,qto, <5i,Ai), i = l , . . . , n , as follows. Definition 3.5 (General distinguishing sequence (GDS)) A GDS for a set of FSMs {Mi,Mn} is an input sequence Xg such that the output sequences pro-duced by all machines in response to Xg € D " = 1 X * , starting from the initial state, are different, i.e., VMi,Mj,i ^ j : X(qi0,Xg) ^ \(qj0,Xg). The generation of a preset GDS can be done by constructing a tree called the general distinguishing tree whose nodes are associated with uncertainty vectors. A n uncertainty vector consists of sets of machines identifiers that are distinguishable ~ by the input sequence from the root to the current node. The initial uncertainty vector, associated with the root, is the set { ( 1 , 2 , ...,n)} which means at this point all machines are not distinguished. The tree expands as follows. For each input in the input alphabet, an edge labeled with the input is spawned from the current node, n\, leading to a new node n2 whose uncertainly vector is generated from ni's according to all machines' output. Machines whose outputs are the same are grouped together. For example, from the initial uncertainty {(1,2,3,4)}, if input x causes Mi's output a, Mi's output b, and M 3 and Mi 's output 80 c, we would get a new edge from the root to a node labeled with {(1), (2), (3,4)}, indicating that M i and M2 can be distinguished by x while M3 and M4 cannot be. This expansion process continues until we encounter an uncertainty vector that contains only singleton states, i.e., all involved machines are distinguished. At this point, we obtain a GDS which is the path from the root to the associated node. During the expansion process, a node may become terminal when no further expansion from there would yield a GDS. This happens when any two machines get to a state pair visited in a previous node. When all nodes become terminal without reaching a node associated with an uncertainty vector of only singleton states, no GDS exists. When this happens, we can try to derive an adaptive GDS (denoted G D S a ) : when a subset of machines have been distinguished from another set, we further distinguish the machines within the subset. Since all FSMs in our situation are pair-wise non-equivalent, G D S a will always exist. The set of these sequences is denoted G D S a . As {(1), (2), (3,4)} is reached with M3 and M4 getting back to their respective initial state, we know that an input sequence starting from x will not be a GDS since it cannot distinguish M3 and M4 after that. However, we may find that the input sequence yx can distinguish M3 and M4. Therefore, if the output for input x was a (or b), we would know that the IUT was M i (or M2). Otherwise, reset the machines and apply yx which would then separate M3 and M4. E x a m p l e Now let's see an example. We will use the example in Figure 3.14 and assume a faulty IUT which, when being applied the same test suite, generates the following output sequence (the one wrong output is in bold face): 81 Table 3.4: Output sequence on G D S a for M i to M 5 Machines b b a c c c b c a a 1 x y x Z Z X 2 x y y X X X X 3 x y y x x y x 4 x y x z z z 5 x y y x x x y c/z c/z b/y a/y c/z c/z b/y a/y c/z a/y a/y c/z b/x a/y c/z c/z b/y a/y a/x c/z a/y b/y b/x a/y c/z c/z a/x c/z c/z c/x b/y a/y b/x a/y b/x c/x b/y a/y Using this sequence as the input to the tool C O V , five solutions are found (Figure 3.16), i.e., even though there is only one wrong output, there are five possible faulty machines for the IUT. None of them are conforming to the specification. To pinpoint which one is the faulty IUT, we attempt to generate a GDS (or G D S a if this fails) for the solution FSMs. Figure 3.17 shows the GDS tree for this example. For each uncertainty vector, the corresponding states for each machine are also marked. This is represented as a state vector and is placed on top of the uncertainty vector in the Figure (note that the uncertainty vector consists of machine identifiers while the state vector consists of state identifiers). As all nodes become terminal before a GDS is found, there exists no GDS for all solution FSMs. However, a G D S Q exists. The sequence bba distinguishes {M\,M±} from { M 2 , M 3 , M 5 j ; the sequence ccc distinguishes M i and M 4 ; and the sequence bcaa distinguishes M2,M^, and M 5 . Table 3.4 lists the outputs of the machines with respect to these input sequences (empty entries imply "don't care" outputs). This allows an adaptive procedure to finally pinpoint the IUT machine. 82 Figure 3.16: Possible faulty machines for the IUT 83 84 As a last note, we point out that it may be possible to employ the idea of disjunction machine as proposed in [34] to handle the problems of incremental test suite generation and fault localization. 3.7 Evaluation of test optimization techniques Another application of our coverage measure is to evaluate some test generation methods whose fault coverage is still uncertain. If the fault coverage is not 100%, our tool C O V can be helpful in investigating the reason and making it complete by providing additional test cases as shown in the previous sections. We chose to study the various UIO based optimization techniques (the results were originally reported in [108]) since they represent a great deal of efforts in reducing test sequence length while the fault coverage loss was neglected. We first give a brief introduction to the four major optimization techniques. 3.7.1 Test optimization techniques The basic method of testing an F S M is to test each transition and identify the final state after the transition. A test case, denoted as TEST(qi,qj\ L) (also called segment in [17]), consists of the input for the testing edge (qi,qj-,L) followed by a characterizing sequence (CS) for state qj, i.e., TEST(qitqj;L) = L®.CS(qj), where 1,0) is the input part of L. Each test segment is concatenated by the use of a reset signal and a shortest path P(qi) from qo to qi to form the overall test suite TS, i.e., 85 TS= X) ri-P{qi)-TEST{quqj]L). This method was used in our previous examples. The optimization techniques focus on how to connect the test cases to minimize the length of the test suite. The reset capability is not required. Test cases can be started one after another, or even overlapped, without having to go back to the initial state. Since UIO sequences usually exist and multiple UIO sequences often provide more room for optimization, UIO is chosen as the CS in all of the four optimization techniques to be analyzed. But where only single UIO is used, other characterizing sequences can also be used in principle. R u r a l Chinese postman method This method was proposed by Aho, Dahbura, Lee and Uyar [2]. It uses the Rural Chinese Postman (RCP) problem in graph theory to minimize the transfer sequence between test cases. It opened a new direction for optimization research. Other optimization methods are basically extensions of this method. In the paper, the authors formulate the optimization problem as follows. The specification machine is represented as a graph G = (V, E). First, a new graph G' = ( V , E') is constructed such that V = V and E' = EL)EC, where Ec = {(Qi,Qk;Li • UIOj)\{qi,qj;Li) G E and 5{qj,UIOj) = Edges in Ec are "pseudo-transitions" that represent all test cases. They have exactly the same number as the transitions in G, and contain all the vertices of V. Thus, the edge-induced subgraph G[Ec] — {V, Ec) is a spanning subgraph of G'. The cost of edges in Ec is defined as the cost of TEST(c[i,qj; Li) which is usually taken to 86 be the total number of edges. Clearly, the objective becomes traversing each edge in Ec at least once with a minimum cost tour of G'. Such a tour is a Rural Chinese Postman tour. The R C P problem is NP-complete for the most general case, but when G[Ec] is weakly connected, it can be solved in polynomial time. In [2], it is pointed out that if an F S M has the reset capability or has a self loop for each state, then G[Ec] must be weakly connected. We have observed that even for machines without reset or self loops, most of them are still weakly connected. This convinces us that the technique has a wide applicability. When G[Ec] is not weakly connected, heuristics will have to be used to find a sub-optimal solution. To solve the R C P problem, a rural symmetric augmentation graph G* = (V*,E*) of G' is constructed such that V* = V and E* contains all edges in Ec, and possibly some edges in E. The idea is to minimize the number of edges chosen from E, and at the same time make the augmented graph symmetric, i.e., for every vertex in V* the in-degree equals the out-degree. Algorithms for minimum-cost and maximum-flow in graph theory can be used to find such a minimal augmentation. The edges in G* can be covered by an Euler tour which can be computed efficiently. The tour is then the overall test suite. In this method, only one UIO sequence is used for each state. The following method which is an extension of this one, employs multiple UIOs for a state to achieve further reduction of test suite length. M u l t i p l e U I O method Multiple UIO sequences are a set of minimal length UIOs for a state. It was found in [87] that using different UIOs for identifying a state in different test cases can reduce the length of the overall test suite. This is because by selecting the appropriate UIOs, 87 the graph G[Ec] can be made closer to symmetry, i.e., the difference of in-degrees and out-degrees for a vertex may be smaller, thereby fewer edges from E are needed to augment it. The problem is also translated into a minimum-cost maximum-flow problem, and heuristics may be needed when the problem is intractable in rare cases. Different UIOs can then be selected for testing different transitions with the same final state. It was shown in [87] that up to 30% reduction of test suite length could be achieved, depending on the properties of the F S M . This is a substantial saving over the single UIO R C P method. Overlaps method Another factor, the overlapping between test cases, is considered in [17] to further minimize the test suite. Single UIO sequence is used. The idea is that if two test cases T i and T2 are overlapped, i.e., the last part of T\ coincides with the first part of T2, then they can be merged with the overlapping part serving both T\ and T2. If T2 is completely contained in T\, then T2 disappears after the merge. The problem is how to maximally exploit the overlapping. In [17], a technique is presented to transform the problem into a minimum cost maximum cardinality matching problem in a bipartite graph. In general, the solution to the problem can be a number of disconnected circuits in the transformed graph. Some heuristics are then used to connect them. Empirical study in [17] shows that this technique results in a significant reduction in the test suite length. 88 M u l t i p l e U I O and overlaps method This technique combines multiple UIO sequences and overlaps to fully exploit the properties of the test cases and yield the shortest test suite. Two such methods were proposed in [17] and [68] respectively. The method in [68] is used in our study as it produces shorter test suite in general. In [68], a machine is called definitely diagnosable if it has no converging edges, i.e., no two edges going into the same state with the same input output label. In this case, the test suite is simply an Euler tour of the F S M graph G (minimally augmented if G has no Euler tour) plus the UIO sequence for the last state of the tour. The rationale is that for such machines, the test suite not only tests each transition but also serves as the characterizing sequence for each state visited. If converging edges exist, a graph G' is constructed by removing the converging edges. Then a set of disjoint paths in G' that covers all edges (only one path if G' contains Euler tours) is computed. The problem becomes how to join these disjoint paths and the converging edges such that the total length is minimal. UIO sequences are used both for joining the paths and also identifying the states along the paths. It turns out that such a problem can be converted to a maximum cardinality minimum cost matching problem for a bipartite graph. If the solution is an Euler tour (or path), then the UIO of the last state is appended to the tour to form a test suite. Otherwise some heuristics are used to connect the disconnected parts. The overall test suite is shown to be a combination of multiple UIOs and overlaps. The examples in [68] as well as our experiments indicate that this is another leap in the optimization. The length of the test suite given in [68] is surprisingly short, typically in the order of the number of transitions in the F S M . 89 State UIO sequence Tail 9o c/z a/y 93 c/z c/z 9i 9i b/y a/y 9o 92 a/y a/y 9o a/y b/y 9i c/z b/y 93 93 a/y a/x 9o a/y b/x 93 a/y c/z 92 Figure 3.18: A sample F S M and UIOs for each state 3.7.2 C o v e r a g e eva luat ion results The fault coverage for optimization techniques was not well studied partly because of the complexity involved with combined faults. We used C O V to conduct an empirical study of the four optimization methods. It was found that optimization can sometimes reduce the fault detecting ability of a test sequence compared to an unoptimized one. C O V was also employed to explain how this could have happened. Figure 3.7.2 is the sample F S M used in our study. It was generated quite arbitrarily. The minimal UIO sequences for each state with different tail states are also given. The first UIO is the one used when single UIO is required. The test suite for the above four optimization methods are listed below: (TI) R C P with single UIO: Length = 45 c/z a/y a/y b/x a/y a/x b/x b/y b/y a/y a/x b/x b/y c/x b/y a/y b/x b/y a/x c/z a/y a/y c/z a/y b/y b/y a/y a/x c/z a/y c/x b/y a/y c/z a/y a/y a/x c/z b/x a/y a/x c/z c/z b/y a/y (T2) R C P with multiple UIO: Length = 38 90 Table 3.5: Fault coverage results for T1-T4 TI T2 T3 T4 Sequence Length 45 38 34 27 No. of indistinguishable FSMs 0 9 8 26 Fault coverage 1 0.1 0.11 0.037 c/z c/z b/y a/y c/z c/z b/y a/y c/z a/y a/y c/z b/x a/y c/z c/z b/y a/y a/x c/z a/y b/y b/y a/y c/z c/z a/x c/z c/z c/x b/y a/y b/x a/y b/x c/x b/y a/y (T3) Overlaps with single UIO: Length = 34 c/z c/z b/y a/y a/x c/z b/x a/y a/x b/x a/y a/x b/x b/y c/x b/y a/y a/x c/z a/y a/y a/x b/x b/y a/x c/z a/y b/y b/y a/y b/x c/x b/y a/y (T4) Multiple UIO and overlaps: Length = 27 c/z a/y a/y c/z c/z b/y b/y b/y a/y b/x c/x b/y a/y c/z b/x a/y b/x a/y a/x c/z c/z a/x c/z c/z c/x b/y a/y It can be seen that T2 and T3 each gains about 16% and 24% reduction in length respectively, with respect to TI , and this is consistent with what is reported in [17, 87]. T4's reduction is 40%, approximately the sum of the effects of multiple UIOs and overlaps. To evaluate the coverage, each test suite is fed to COV. Note that no reset capability is assumed (the test tree is in its degenerated linear form). The results are listed in Table 3.5 (See Appendix C for all solution FSMs). This, together with some other experiments, leads to the following observa-tions. 91 Observation 3.1 Multiple UIOs, as well as overlaps, can sometimes cause loss of fault coverage. The two optimization methods are comparable in length reduction as well as in coverage loss. The use of both techniques is likely to cause a higher coverage loss than when either one is used alone. Let L^ represent the sequence length. Our examples show that LTI > LT2 « LT3 > LT4, and FC(T1) > FC(T2) « FC{T3) > FC(TA). While this may not be a general conclusion, the differences in test suite length and fault coverage are obvious enough to justify a clear tendency. There were some experiments where multiple UIO or overlaps did not reduce the original fault coverage. For T4, however, all examples showed a coverage loss. As can be seen, during test suite generation, different test suites (with the same length) can be produced because of the multiplicity of Euler tours in a graph. The maximum flow minimum cost may also have different edge sets. This led to our next observation. Observation 3.2 The choice of different solutions for the transformed graph prob-lem could lead to test suites with different fault coverage. In other words, the order of connecting test cases in forming the test suite has an effect on fault coverage. For example, the following test suite (T2a), which was obtained using a different Euler tour for T2, has only 4 indistinguishable FSMs instead of 9. In other words, it has a better fault coverage than T2. c/z c/z b/y b/y b/y a/y a/x c/z a/y c/x b/y a/y b/x a/y (T2a) b/x a/y c/z c/z a/x c/z c/z b/y a/y c/z a/y a/y c/z b/x a/y c/z c/z b/y a/y c/z c/z c/x b/y a/y 92 In contrast, in the unoptimized method of constructing the test suite when reset is available, the order of the test cases ri • P(qi) • TESTfa, qj',L) is irrelevant with respect to the fault coverage of the test suite. This is because the test tree is uniquely determined by the test cases independent of their orders. However, the choice of P{qi) does influence fault coverage. For example, in Figure 3.2, if we had chosen 6/1 as the preamble to state 2, the final test suite would have no indistinguishable solutions. This behavior is consistent with Obser-vation 3.2. Observation 3.3 For FSMs with a reliable reset capability, the choice of preambles in the test cases could affect the fault coverage of the test suite. Discussion To understand how some faults "outsmarted" a test suite, we examined some of the indistinguishable FSMs. Figure 3.19 shows three such FSMs with respect to T2. Note that in Figure 3.19(b), there are two transfer faults: (Fl) (91,93; c/x), and (F2) (93,93; b/y). Figure 3.19(c) has three faults: a transfer fault (F3) (91,92; a/x), and an output fault concurrent with a transfer fault in one edge: (F4) (91,93; c/z). Figure 3.19(d) is a weird mutant with transitions radically different from the original F S M . It would be hard to construct this indistinguishable F S M without the tool. In Figure 3.19(b), when the original edge (91,91; c/x) is tested, the UIO sequence (b/y a/y) intended to identify 91 is also acceptable by 93, the tail state of F l , due to F2. When F2 is tested by applying (b/y b/y a/y) at 93, it again fools us by giving the same outputs. As the tail state for this UIO is not changed by the faults, other test cases are not able to exercise the faulty edge. T2, which connects 93 (c) Indistinguishable FSM2 (d) Indistinguishable FSM3 Figure 3.19: Three indistinguishable FSMs with respect to T2 94 test cases with two more edges that are not the faulty ones, thus fails to expose the faults. Clearly, this type of faults may also escape detection by the single UIO R C P method. T I happens to be able to defeat this faulty machine because it has the right transfer sequences. Interestingly, if we had chosen a different transfer sequence by intentionally avoiding faulty edges, T I would also fail. This indicates that although the use of multiple UIO sequences reduces the length of transfer sequences, it also decreases the probability of capturing some faults. The same is true for overlaps. Figure 3.19(c) shows another way we could be "cheated" by a faulty machine. When testing F3, the test case (a/x c/z c/z) brings the machine to 93. T2 happens to use (c/x b/y a/y), which is acceptable by 93, to test the outgoing transition c/x from qi right after (a/x c/z c/z). Instead of testing the transition c/x from q\, the transition c/x from 93 is tested. Other test cases again do not touch the faulty edges. This phenomenon is generally referred to as fault masking, where several faults are combined to mask each other. It can be seen that different ordering of the test cases could lead to different ways of fault masking, hence possible different fault coverage values. The F S M shown in Figure 3.19(d) is difficult to interpret as the transition pattern differs greatly from the original specification. The simple patterns of fault masking shown in Figure 3.19(b) and 3.19(c) as explained above are unable to unravel how the faults escaped detection. It seems to suggest that no general patterns of fault masking could be found to explain all undetected faults. Lombardi and Shen [66] studied some patterns in a specification F S M that can cause fault masking. This will help in avoiding fault masking, but still the patterns may be incomplete, i.e., there could be some other patterns that can also cause fault masking. As we observed, coverage loss is aggravated by optimization techniques, es-95 pecially when multiple UIO sequences and overlaps are used together. We attribute it to the increased fault masking effect caused by arbitrary combinations of the test segments. The arbitrary choice of preambles and transfer sequences as well as the ordering of the test cases, may also result in a test suite with weakened fault cover-age. This is possible because all test suite generation methods are based on a correct specification while the UIO sequence and an optimized sequence, unlike a DS or a W set, cannot guarantee trace equivalence between the specification and a machine that accepts the sequence. To solve this problem, we suggest that an optimized test suite be checked with COV for its coverage. If it is not complete, additional test cases can be generated to distinguish those T-indistinguishable machines as shown in previous sections. In the next chapter, we will extend our coverage measure to the testing of communicating finite state machines. 96 Chapter 4 Coverage measure for testing embedded modules We have developed our coverage measure for single machine testing and explored its various applications. However, many protocols are specified as a system of com-municating modules, and it is often hard to isolate single modules for testing due to their close integration into the whole system. In such a case, the module is embedded in the composite system and exposes no interface to the tester. This re-stricted observability and controllability of the module under test (MUT) presents new issues to the tester, which must endeavor to show the correctness of the M U T without direct access to it. This problem leads to our work on coverage based test-ing of embedded modules. The method extends naturally to the testing of a system of communicating machines where testing can be performed successively on each module within the system. In this chapter, we focus on developing our coverage measure for an embedded module. This measure forms the basis for testing a composite system in a successive 97 manner and for testing embedded modules as in the embedded test method (Figure 2.2). 4.1 Introduction Real life protocols are often complex and structured, which makes it infeasible to test them as a single monolithic module, since it would require composition of all components and easily lead to state explosion. Testing each component module with conformance would guarantee the conformance of the composite system [61]; however, due to the fully integration of many systems, it is sometimes impossible to single out a module and testing it separately. This is often seen in distributed component computing and embedded systems, where components are embedded in a composite system and don't offer an interface of its own. To test such a system, we adopt the approach of successive testing, where each module is tested under the assumption that all other modules are correct. When all modules are tested this way, we conclude that the composite system is tested. This incremental approach allows the tester to focus on one module each time, and avoids the problem of state explosion. The constraint, however, is that the tester has to infer the conformance of the embedded module from the external behavior of the composite system. This type of testing is known as embedded testing as in the International Standards Organization (ISO) conformance testing framework for communication protocols [52]. Most work in the area of protocol testing has mainly been on single compo-nent testing where each component of the system is tested in isolation. Effectiveness of such tests can be evaluated in various ways, ranging from fault simulation [24, 90], structural analysis [107], to faulty machine identification [101, 109]. Recently some 98 work aiming at testing embedded components (also called testing in context) has appeared [78, 79, 77, 53]. The work so far has mainly been on defining fault models and generating effective test suites with respect to given fault models. In our work, we attempt to define a measure to evaluate the coverage of a given test suite for embedded component testing, and to produce test suites based on the measure. The traditional fault simulation method as used in fault coverage evaluation for isolated machines [24, 90] may be adapted for use in embedded systems by defining an appropriate fault model as in [78]. However, it has the same difficulty in that for many complex systems detailed fault classes are unknown or are difficult to be established. We therefore propose to extend our coverage measure as described in Chapter 3 to the evaluation of test coverage for embedded system testing. The approach inherits the pros and cons of the measure but with the additional advantage that no global identification is needed. Besides, it may be used in the factorization of finite machines. In the following sections, we first give an overview of the general principles of embedded system testing and test architectures. The coverage measure in embedded testing and its calculation is then described. 4.2 Embedded test architecture We model a composite system as a system of communicating FSMs, one being the M U T , and all others being the test context. Refer to Figure 2.1, the tester exercises the behavior of the M U T via PCOs, with the test context interacting with the M U T via IAPs. This architecture can be refined in Figure 4.1. The slight difference with that in [79] is that we allow the M U T to expose interface in general. In a pure embedded M U T , it only interacts with the test context. 99 System under test MLT U Test context Test suite X Specification Verdict Testing system pass fail PCO events: X, Y; IAP events: U, Z. Figure 4.1: Test architecture for embedded testing 100 The tester contains a test engine that applies test suites to the system under test (SUT). The response of the system is compared with the expected response according to the specification, to determine whether the SUT conforms to its spec-ification. A verdict of pass or fail is given from the comparison. The test context is a set of FSMs that are not being tested; instead they act as an environment in which the M U T runs, and which interacts with the MUT through the IAPs. The IAPs are not directly controllable or observable by the tester. Based on this architecture, we can represent the MUT with the machine M = {Q, X U U, Y U Z, qo, 6, A), and the test context with the machine C = (S, X U Z,YLlU, SQ, A, A). The composite system SUT can be defined as a system of CFSMs comprised of M and C. Without loss of generality, in the following sections we assume that external inputs X, external outputs Y, and internal interactions U and Z are all distinct. We also use lower case letters x, y, u, z with possible subscripts to denote individual input or output action as a member of their corresponding capital letter sets. Also, during testing, only steady states are observable, so we adopt the I/O ordering constraint which allows the next test input to be applied only after the system has produced an external output and entered into a steady state, and is waiting for an external input. 4.3 T h e coverage measure Recall that in Definition 3.3, coverage is defined as the inverse of the number of T-indistinguishable machines, i.e., Cov(Ms,T,n) = l - —. KTCM — K-SCM + i 101 where Ms is the specification of the IUT, T a test suite, and n the upper bound of the number of states in the IUT. Calculation of the measure boils down to: • Calculation of KTCM-, i-e., to identify the number of machines that accept the test suite (T-conforming machines), and • Calculation of KSCM, to determine how many of these TCMs actually conform to the specification. The application of the coverage measure to embedded testing requires the calculation of KTCM and KSCM under the new constraints where the IUT (or MUT in this case) is only accessible via the test context. We elaborate the calculations in the following sections. 4.3.1 Calculation of KTCM In the single machine case, the calculation of KTCM is done by construction of T-conforming machines under the "upper boundary" assumption on the IUT's states. Moreover, in order to construct the T-conforming machines deterministically, they must be modeled as deterministic finite state machines, using either the Moore or Mealy model (the latter is commonly used in communication protocol modeling). In embedded system testing, the coverage could have been calculated by identifying the whole global system. However, this approach would not be interest-ing because it may be unable to handle a complex composite system due to high computational cost. Besides, when we assume the test context is faultless (which is perfectly reasonable in embedded system testing), it is simply unnecessary to iden-tify the global system because a) some faults in the MUT are masked by the test context, so they are not detectable from the external system behavior; and b) a lot 102 of computations would be wasted in identifying possible faults in the context. We therefore propose an approach that identifies the M U T only, based on the test suite applied to the composite system. Let Mi be the embedded M U T module to be identified given its specification S, the test context C, and the test suite TS. Mi is assumed to have the same input and output alphabet as S. We consider TS as comprised of a linear sequence of test steps (I/O pairs). If a test suite consists of test cases starting from the initial system state, a special input reset is used to bring the system to its initial state, regardless of its current state. This initial state is a combination of the initial states of the context machine and the M U T . Whenever reset is encountered, both the context and M U T are set to its initial state, and no output (or a null output) will be produced. The faults in the M U T will not affect this capability. Our task is to infer the output and next state functions for Mi based on the test suite. The approach is to first build a test tree for Mi, denoted TT, which represents all sampled behaviors of Mi as excited by the test suite (via the test context). This test tree is then collapsed for the identification of Mi using the approach described in Chapter 3, which will give us all T C M s . We follow the following steps to build the test trees. 1. Apply a test step x/y (an I /O pair) in the test suite to the system. Since C is known, reachability computation can be performed until the input reaches Mi (we do not exclude the case where an input is directly applied to an embed-ded module by bypassing C; this is done simply by skipping the reachability computation part). For example, an input x applied to the system via C may produce an internal event in C as an input to M / . A special case in this step is the reset signal. No reachability computation is needed; we simply reset the 103 context machine and move to the root of the current test tree. 2. When an input reaches Mj, we start to construct TT for M j . At this point, the output caused by that input from C may be any possible event that is allowed in M/'s output alphabet. Try each possible event according to the next step. 3. For each possible event op, continue the reachability computation of Step 1, until an external output is produced. If, during the reachability computation, an output of the context is an input back to Mj, Step 2 will be called. This will lead to a recursive execution of Steps 2 and 3. When an external output is finally produced, it is compared with the output of the test step. If they are different, a contradiction is found and hence op is ruled out. Repeat this step for the next possibility until an external output compatible with the test step is observed or no possibility is compatible. If a compatible output is found, TT goes one step farther with a label of i/o, where i is the internal input to Mj excited by the global input, and o is the compatible output. If no compatible output can be found, backtrack to the previous test step. TT is also "rewound" accordingly. 4. If all test steps have been processed, we have obtained a test tree TT for M / . At this point, we save TT and backtrack to the previous test step, with C and TT being set to their respective previous states, and continue searching for the next output possibility with respect to these states. This step is repeated until all output possibilities have been exhausted, resulting in all test trees for Mi. Figure 4.2 gives the algorithm for constructing the test tree. It is a recursive 104 procedure that processes the test suite one test step each time. The inputs to the algorithm are the initial state of the M U T to be identified, the initial state of the context, and the test suite. In other words, we build our test tree starting from the initial state of the system. The output is the set of test trees for the M U T , obtained by applying the test suite to the system within the given test context. The first line checks if the whole test suite has been processed. If so the test tree has been constructed and is saved, and the algorithm backtracks to search for other solutions. Line 2 handles the special case of the reset signal, resulting in the initialization of the context as well as the current test tree. The current tree node points to the root. Line 5 applies reachability computation (RC) from the global input until the M U T module Mi is reached, which means an internal input for M j is produced from the global input. In case where a global output is generated before Mi is reached, i.e., this test step does not really test any part of M j , the procedure backtracks to the next test step without adding any edge to the test tree. Otherwise, the algorithm proceeds to line 8 to search for an output symbol for a potential edge in the test tree. This is done by analyzing all possible outputs for Mi with regard to the present internal input. In line 9, for each output possibility, if it is a context input, the algorithm goes back to Line 5 for further reachability computation. If it is a system output instead (line 10) and it is consistent with the output given in the test step, we have found a potential edge for M j . However, due to backtracking, the edge for the node pair may have been generated before, which may or may not be consistent with the current edge label (ai/bi). If consistent, nothing needs to be done; otherwise we have to backtrack since some previous step that causes the inconsistency must be undone. In line 15, if all attempts failed, we go on to try the next output b{. If no compatible b{ can be found, which indicates an inconsistent 6j 105 Algorithm 4.1 (Test tree construction for Mi) a — ( c i , o n ) : the test suite, where Oi = Xi/yi is the ith test step; v^: represents tree node i; qi: represents state i of the context; Z: the output alphabet of Mi;. TT: the test tree being constructed. boolean Test Tree (&i,Vi,qi) { 1. if (oi = NULL) then { save TT; return FALSE;} 2. if (oi = reset/null) then { Uj «— v$; qi qo; } 3. else { 4- in <— Xi; 5. RC from in to Mi; Context reaches qj with input k; 6. ai 4-\(qj,k); 7. if (ai is input to Mi) then { 8. for bi € Z do { 9. if (bi is input to C) then { in <— bi; goto 5 }; 10. else if (bi = j/j) then 11. if edge Vi Vj already exists then 12. if bi = b\ then break; else return FALSE; 13. else { add edge Vi ^» Vj to TT; break; } 14. } 15. if (no compatible y found for all bi) then return FALSE; 16. } 17. else if (ai is system output and ^ yi) then return FALSE; 18. } 19. return TestTree(oi+i,Vj,qj); Figure 4.2: Test tree construction algorithm 106 C M, X u A v' X v w > y z/u z 6 b Composite system Figure 4.3: Test tree construction for embedded component in a previous test step, the algorithm backtracks. Line 16 repeats the processing for the next test step. If the test suite was correctly generated for S, we will end up with at least one test tree for Mi (because there must be at least one machine accepting the test suite); otherwise the algorithm will produce no test trees which would indicate an incorrect given test suite. Figure 4.3 gives a simplified illustration of this process. Suppose a test step consists of x/y. The external input x causes a transition x/u in C, in which u serves as an internal input to M / , which outputs y. An edge labeled u/y in TT is then obtained. The dotted line from Mi to C indicates a possibility where Mi produces an output to C in response to its input. In general, a finite number of events may be exchanged between C and Mi before an external output is produced. However, when constructing the test tree, since we cycle through all possible outputs when determining an edge, the test tree could be potentially infinite. This leads to the issue of "loop prevention". 107 Loop prevention A loop happens during test tree construction when the context and the test tree keep exchanging internal events without producing an external output. Take the example in Figure 4.3, for the self-loop labeled z/u. When generating a TT edge with input u, if the output for u is chosen as z, C and TT would be stuck in an endless loop exchanging u and z. This would cause an infinite test tree and Algorithm 4.1 not to terminate. To prevent this from happening, we must identify the conditions under which this can happen, and then find out ways to prevent it. A n examination of the problem reveals that if the context contains cycles consisting of only internal events, it can cause a loop. A cycle is a transition path whose end state is the same as the start state. We call a cycle with all internal transitions as an internal cycle, or i-cycle for short (similarly, i-path for internal paths). We prove the following theorem: Theorem 4.1 A loop between the test context and a test tree can happen if and only if there exists i-cycles in the test context. Proof: 1) i-cycles loop. Suppose there is an i-cycle in (Z/U)* in the test context C. Pick a state q\ on the cycle, which is z\ju\, z2/u2, ...,zn/zn (Figure 4.4). When C gets into q\ via some external input, let the test tree TT be at node n\. For C's output ui, TT may select z2 according to Algorithm 4.1, which causes C to output u2. TT may select z-& for u2, causing C to output U3. This may continue until C gets back to state qi, and TT repeats the path from n i . Therefore, there is a loop between C and T T . 2) no i-cycles no loop. Suppose there is a longest i-path in C, which is 108 C: TT: nl •6 (1) i-cycle => loop (2) no i-cycle => no loop Figure 4.4: Proof for Theorem 5.1 IT = z\/u\, Z2/U2,Zj/ui. Let C enter state qi after Zi/ui. The outgoing transitions from qi must be of the form x/y, x/u, or z/y, since otherwise ix would not be the longest i-path. For transitions of the form x/y and x/u, since x is an external input, it must be a test input from the test suite, and TT stays at the same node with no new edge introduced, i.e., no loop will happen. For transitions of the form z/y, TT would have selected z, and y will be produced by C. This external output y is then compared against the test suite, and TT has a new edge Ui/z added. This continues until all test steps are exhausted at which point TT is terminated. Therefore no infinite loop will exist between C and TT. • This theorem identifies the sufficient and necessary conditions for loops to exist. The next step is to find techniques to prevent loops once we recognize that they may happen. The first step toward this goal is to identify all i-cycles in the test context. If there are i-cycles, we have to employ some means to prevent loops from happening when constructing test trees. Identification of all i-cycles C can be done in two steps. First, we color all internal transitions, i.e., those labeled with internal actions u/z. Second, we do a 109 Canonical i-cycles: s0-zl/u2->s2-zl/ul ->s0; si - z2/u2 -> s3 - z2/ul -> s2 - z2/ul -> si; s3 - zl/u2 -> s3. Figure 4.5: Canonical i-cycles standard depth-first search of C but only those colored transitions are traversed. An i-cycle is detected if the search reaches a state that is already traversed. All i-cycles found this way are not overlapped and are said to be canonical. For example, the machine in Figure 4.5 has three canonical i-cycles. When i-cycles appear in the context, construction of a test tree needs to be loop preventive to avoid an infinite test tree. Suppose there is an i-cycle, £ = zi/ui, Z2/U2, -., zn/un. We call a sequence ui/z2,U2/z$, ...,un-i/zn,un/zi the complement of £ and denote it £. It is the path in the test tree corresponding to £. In order to avoid a loop, the test tree in construction must not contain the path £. This can be done by recording the path in test tree and whenever a new edge is added, compare it against complements of all i-cycles. The recording starts when the context enters into a state on an i-cycle. The test tree avoids the last step of an i-cycle complement by simply not choosing the output of that last step. This way the loop is broken and the test tree can be terminated in finite steps. To summarize, in order to avoid loops between the test context and the test tree, we do the following: 110 • Use depth-first search to identify all i-cycles in the test context; • Generate complements of the i-cycles; • During test tree construction, avoid the i-cycle complements. We integrate this technique into Algorithm 4.1 to generate finite test trees. The trees are then fed to the tool COV to produce all T-conforming machines, which gives us the value of KTCM-4.3.2 Calculation of KSCM The calculation of KSCM depends on the conformance relation used in determining whether a T C M conforms to the specification. In the single machine case, the strong equivalence, quasi-equivalence, and the reduction relations are used as conformance relation for complete DFSM, partial DFSM, and NDFSM specifications. However, in the case of embedded testing, conformance has to be determined at the composite system level. This is because with limited controllability and observability of the MUT, we can only determine a module's conformance by its globally observable behavior. If an MUT does not conform to its specification at the component level, but the global behavior of the MUT in composition with the context conforms to the composition of its specification and the context, we can only conclude that the MUT works correctly in that context. The context can be considered tolerant or a mask for some faults in the MUT. We call this conformance in context, and denote it as conf c. The observational equivalence relation [1] applies in this situation and is used for determining the conformance in context. Let C and S be the context and specification machine respectively. An implementation of S is M / . Under the I/O ordering constraint, we only deal with 111 stable global states in the composition of C and Mj, denoted C o Mi (since only stable states are observable and/or controllable by the tester). This composition is obtained from the reachability graph (i.e., the product machine CxMi) by removing internal transitions and collapsing transitions carrying external input and/or output. Conformance in context can be expressed as: M/confcS iff C o Mi conf C o S. where conf is the conformance relation as used in the single machine testing. Con-sequently, KSCM = \{M\M e T C M A Mconfc S}\. Note that in order for C o S to exist, there must be no livelock between C and S. If livelock exists, C and S may exchange internal events indefinitely without reaching any stable state. We assume that this has been verified during system design, which should prevent this type of no-progress cycles from appearing in a sound system. The existence of C o M / , however, is not guaranteed by the absence of infinite loops between C and M/'s test tree. The livelock between C and M / , if it exists, can be detected during the composition. When a livelock is detected, the Mi is considered to fail the test suite since a tester can discover the livelock with a timer. The composition algorithm for two machines are presented in Figure 4.6. Instead of generating the product machine and then extract the composed one, the algorithm builds the composed machine directly from reachability computation. The idea is to compute all reachable states starting from the initial state but only save the stable states. Transient states are discarded after the transition label between two stable states has been derived. This avoids building a complete product machine 112 and saves space in storing transient states. During the composition, livelock can be detected, which happens when a cycle comprised of only transient states is encountered. This is done within the function next-state. A transient state is represented as a four-tuple (c/i, q2, el , e2), where q\, q2 are the states of each component machine M\ and M2 respectively, and ei, e2 are the events at the input queue of M\ and M2. Since in our model, no global inputs will be applied until a global output is produced, an event at the input queues is consumed right after it is placed on the queue. Therefore at any transient state, there is at most one event on the queue. This allows us to use the above four-tuple to represent a transient global state, where at most one event appears at each queue. Note that we need at most m elements in the set LIST to save transient states, where m is the maximal number of continuous internal interactions between the two machines. The space for LIST is released after the function returns. The final composed machine, which exists if no livelock was found, may contain equivalent stable states, i.e., those not distinguishable from external I/O behavior, so the last step is to minimize it to obtain a reduced composite machine. Minimization can be done with the standard machine minimization algorithm such as that in [59]. Figure 4.7 shows an example where the machines in (a) and (b) (taken from [78]) are composed to generate the machine in (c) which is minimized to machine (d). With the composition algorithm in place, the calculation of KSCM is straight-forward: each time an Mj is generated by COV, we compute Co Mi and compare it with for conformance if it exists (i.e., no livelock detected). If Co Mi doesn't exist, this Mi is discarded from the solution set since it will fail to pass the test suite. A l l M/ ' s that conform to the specification in context are counted as KSCM-113 Algorithm 4.2 (Composition of two FSMs) Input: Two FSMs Mk = (Sk,Xk,Yk,sk,Sk,Xk), k G {1,2}. Output: Composition of M i and M2 • compose (Mi,M2) { 1. enqueue ((si,s 2)); 2. while queue is not empty do { 3- (91,92) <- dequeue(); 4- for Va; G external input do { 5. (9i>92) *~ next-state (q\, q2,x); 6. if livelock was detected then exit. No composition exists. 7. if (q'i,q2} is a new state then enqueue (gi,^)/ 8. } 9. } next-state (qi,q2,x) { 1. LIST <— cp; /* LIST stores transient global states visited */ 2. a*r- x; 3. if a e Xi then { 4- if {S(qi,a),q2) G LIST then livelock detected; exit. 5. y <-\(qi,a); qi <-6(qi,a); 6. LIST 4- LIST U{(qi,q2,0,y)}; 7. } else 8. if a G X2 then { 9. if (qi,S(q2,a)) G LIST then livelock detected; exit. 10. y 4- X(q2, a); q2 4 - 5(q2, a); 11. LIST*- LIST \J{{qu92,y,0)}; 12. } 13. if y is external output then return (qi,q2); 14- else { a «— y ; goto £ }; i J . } Figure 4.6: Composition of two FSMs 114 (c) Ml comp M2 (d) reduced Ml comp M2 F igure 4.7: Compos i t ion of two machines 115 4.4 Computational complexity of the measure We already know from Chapter 3 that the calculation of the coverage measure Cov(Ms,T,n) is no better than NP-complete. We now ask the following question: Given a test suite T, and the test context C, is there a machine M with n states such that the composition of C and M agrees with T? Note that here the composition operation is what we used in Algorithm 4.2 with only stable states considered. This question is central to the computation of our coverage measure, since during the construction of TCMs, we essentially try to find machines that accept the given test suite after composition with the test context. We claim that it is NP-complete to answer the above question, which implies the hardness of the coverage measure computation. Theorem 4.2 Let T be a test suite, C the test context. It is NP-complete to decide if there is an n-state machine M, which interacts with C via a predefined channel, such that the composition of C and M accepts T. Proof: Call this problem ESAT. First we show that ESAT is in the domain of NP. A non-deterministic algorithm can guess a solution machine M for ESAT, and then check if the composition of C and M accepts T. Suppose the length of T is I, the checking can be done by applying the test steps one by one. For each test step, the function next-state in Algorithm 4.2 can be used to handle transient states. If a livelock is detected, the checking halts with answer "no"; otherwise the test step can be verified in 0(m) time where m is the number of internal exchanges between C and M. The whole test suite can then be checked in 0(lmmax) where mmax is the maximal number of internal exchanges for all test steps. Therefore, the checking of whether M is indeed a solution can be performed in polynomial time. 116 Context MUT Figure 4.8: A special case of E S A T Now we show that E S A T contains a known NP-complete problem as a special case. Consider a restriction of E S A T : the context machine C is a one state F S M as in Figure 4.8, and the internal interactions between C and a M U T is X' and y' , which are simply a renaming of X and Y respectively. Under this restriction, C is essentially a "pass-through" module, and E S A T becomes the single machine identification problem which is known to be NP-complete [37]. • The NP-completeness of the E S A T problem indicates that it is unlikely that there are polynomial algorithms to compute our coverage measure (if there are, we would be able to solve the E S A T problem in polynomial time). Therefore, heuristics may be the best approach to achieve good performance for a specific case. On the other hand, protocols should be designed as structured with smaller components and large monolithic systems should be avoided. 4.5 T o o l set a n d e x a m p l e To validate the approach, an experimental tool set called E C O V (Figure 4.9) has been implemented in C. It consists of tools for test tree construction ( T T R E E ) , ma-117 chine identification by the test tree (COV), and the composition algorithm (COMP) that checks the observational equivalence in context. In the tool set, C O V has been presented in Chapter 3 and is integrated into E C O V via I /O files. E C O V takes as input a test suite, a test context, and the M U T specification, and produces a cover-age value and non-conforming machines which may be used for further analysis and test suite enhancement. To illustrate the approach, we use the simple example in Figure 4.10 which is taken from [78]. The test context C takes inputs x\, x2 from the system environment and internal input z\,z2 from the component under test, and generates system outputs yx, y2. C also generates internal outputs u i , u2 as inputs to S. The composed machine S o C is generated by determinizing the product machine S x C under the I /O ordering constraint. We use the following test suite from [77] for the component S. This is a com-plete test suite with respect to the fault model where faults in S's implementation do not increase the number of states: coverage faulty machines Figure 4.9: E C O V tool set T = { 118 Composite system x2/ul zl/ul yl y2 (a) System under test (b) Test context C u2/zl ul/zl (c) Component S (d) Composite machine SoC Figure 4.10: Example composite system 119 Figure 4.11: Test tree generated for the embedded component r/- xl/yl xl/yl xl/yl xl/yl xl/yl x2/y2 r/- xl/yl xl/yl xl/yl x2/y2 r/- xl/yl xl/yl x2/y2 x2/yl xl/yl x2/yl r/- xl/yl xl/yl x2/y2 x2/yl x2/y2 r/- xl/yl x2/y2 xl/yl xl/yl x2/y2 r/- xl/yl x2/y2 xl/yl x2/y2 r/- x2/yl x2/y2 xl/yl xl/yl x2/yl xl/yl x2/y2 r/- x2/yl x2/y2 xl/yl xl/yl x2/yl x2/y2 r/- x2/yl xl/yl xl/yl xl/yl x2/yl r/- x2/yl xl/yl xl/yl x2/y2 r/- x2/yl xl/yl x2/yl xl/yl xl/yl x2/y2 r/- x2/yl xl/yl x2/yl x2/y2 x2/yl r/- x2/yl x2/y2 xl/yl x2/y2 120 (a) Ml (b)M2 Figure 4.12: Two FSMs observationally equivalent with S Our tool yields a test tree for S as shown in Figure 4.11 (note that the test context contains one i-cycle: the self-loop z2/u2 at state a). This tree is further fed into our tool C O V to be collapsed into FSMs. C O V produces 19 FSMs, one of which conforms to S at the module level, while the rest, although do not conform to S, are found to be observationally equivalent with S within context C, i.e., the composition of those FSMs conform to the composition of S and C. Therefore, there are no non-conforming solutions at the composite system level, which leads to the conclusion that T is indeed complete with respect to the embedded testing architecture. Figure 4.12 shows two of the generated FSMs M\ and M2 that do not con-form to S at the module level but do at the system level, i.e., Mi - i c o n f S, but Mi c o n f c S. The first one has only two states, yet it is considered conforming when tested in context. This allows us to discover the smallest F S M that implements S without causing system behavior discrepancy. The second one differs from S wildly but still exhibits observational equivalence at the system level. 121 4.6 Extension to multi-module test context So far we have focused on the case where the test context is modeled as a single finite state machine. It is considered as an abstraction of all modules other than the one under test. Consider the more general case in which the test context consists of multiple modules. We can compose all of the context modules into one module and apply our approach as described in prior sections. During composition all global input and output, plus the interactions with the M U T , are considered as external input and output for the context modules. Algorithm 4.2 can be easily extended to handle this case. Again we only maintain the stable states for the collapsed context, and internal actions are removed. The complexity of the composition may be reduced in some cases with an incremental composition. With this method, we first compose two or more machines that are tightly coupled (so that the composite state space can be reduced), minimize it, and then compose it with the remaining machines. The method has been shown effective in validation models that only use rendezvous communications [49]. It will also be effective in our context where asynchronous communications are used, since we only consider stable states which will remove all internal actions and the rendezvous points. In the next section, we will apply our approach to a real life protocol, ex-tracted from a universal personal computing system. It is a protocol modeled as multiple communicating machines (modules) and serves to demonstrate our ap-proach in practice. 122 4 . 7 T e s t i n g o f a u n i v e r s a l p e r s o n a l c o m p u t i n g s y s t e m In this section, we briefly review the universal personal computing (UPC) system which we developed to support personal mobility on the Internet. U P C is modeled as a set of communicating objects distributed on the Internet, with some objects invisible to the outside world. Testing of those objects in an embedded manner presents a suitable application of our method in a multiple module setting. 4.7.1 The universal personal computing system The universal personal computing (UPC) system that we developed [110, 64, 63, 93, 94] supports nomadic computing on the Internet by allowing mobile users to access their personalized computing resources anywhere on the Internet using any available terminals. Since U P C must deal with heterogeneous systems in a mobile environment, independence of computing platforms and support of portable objects are imperative. The system is modeled as distributed objects with C O R B A as the common bus that facilitates distribution, interfacing, and integration of the objects. The development of the U P C system was sponsored by Motorola. The system was formally specified in SDL and verified with an SDL tool called ObjectGEODE. A prototype was also implemented using Java and VisiBroker for Java, an O R B product by Visigenic (now Inprise). In this thesis, we will use a restricted version of the system as an example for embedded testing. This restricted version only considers the case where the user moves while the terminal is fixed. System architecture We only briefly overview the U P C system architecture in this section. Details can be found in the references given above. 123 The purpose of our U P C system is to support nomadic computing on the Internet independent of user's location, motion, and platforms. The essence of such a computing paradigm is to retain one's personal computing environments and access capabilities wherever one happens to be. Typically this is achieved by physically carrying a computing device such as a laptop, palmtop, or a P D A with appropriate Internet connectivity (wireless or wired links) and possibly IP mobility support such as mobile IP [29]. In U P C , we support a broader range of mobility by allowing the user's per-sonal computing environment (PCE) to move with him when he uses any available terminal on the Internet. A n example is that when one travels at an airport, where public Internet-ready terminals are installed for travelers to use, one can use any idle terminal to access the network as well as his own computing resources within a familiar environment, as if he was using his home machine. He would not need to worry about the hardware and software platforms of the terminal. This particular form of mobility is called user mobility as opposed to the terminal mobility where the physical device migrates. The public terminal used by a visitor is called a, foreign terminal, which resides on a foreign network. Correspondingly, the mobile user has a home network which he normally connects to at home. A simplified U P C architecture is presented in Figure 4.13. The foreign ter-minal or its associated host is assumed to be able to house a terminal agent and a Java virtual machine, and to support a graphical user interface. From an object-oriented view, the U P C system consists of the following major objects: user agent, user profile, terminal agent, terminal profile, and facilities. There is a process called initial agent on the foreign terminal, that provides an interface to the mobile user, and a stand-alone application in the home network 124 Figure 4.13: U P C architecture 125 that manages the P C E , allowing mobile users to register, update or delete their PCEs. The P C E manager itself may also be brought to a foreign site allowing a mobile user to update (but not to create or delete) her P C E on site. The terminal agent resides in any foreign terminal that supports U P C , while the user agent sits at the user's home network and keeps track of the user profiles. When a user logs into a foreign terminal with her logical user identifier (LUI) and password, the initial agent calls the terminal agent to locate the user agent for the user, authenticate the user, and obtain the set of home services that the user wishes to bring in (which has been registered in the P C E in advance). This set is compared with the terminal profile to determine the services that this terminal is capable of supporting, in terms of, say, terminal hardware constraints such as colors and resolutions. The terminal agent also checks with the local service providers to see if the above services are also available locally, and gives the user a choice of using it locally if available. The user interface will display two set of services: 1) those available at home, and capable of being supported by the foreign terminal; 2) those available at the foreign network locally. The user can then choose the service she wants, and the system will bring in the P C E as required and run applications (download first if necessary) to provide the desired service. The user interface also allows the user to query the local service provider for any other locally available services or facilities, based on the service types and attributes that she specifies. This accomplishes our virtual global U P C network. System object classes The major object classes in the U P C system are: 126 • those residing in the user agent machine of the home network: user's P C E and user agent; and • those residing in the foreign terminal: terminal agent, terminal profile, and the user interface provided by an initial agent. In C O R B A , server object interfaces are specified in the Interface Definition Language (IDL) which is part of the C O R B A specification. We use the Java/IDL mapping in our system. Personal computing environment A P C E is defined for each user. It consists of a set of objects that the user wants to use when being away on a foreign network using a foreign terminal. Ex-amples of such objects include: application objects that provide certain services, resource objects such as files, and environment objects that define service configura-tions and preferences. The P C E objects will be managed by the User Home Agent (UHA). Mobile users are required to provide and register their P C E s with the U H A . User home agent The U H A is an object that manages the P C E objects for users in a domain and also communicates with the User Terminal Agent (UTA) in authenticating a mobile user and transferring the P C E to the foreign terminal. Each U H A is registered in the C O R B A Naming Service with a binding to a domain name. This allows the U T A to locate it after a user logs into the foreign terminal using an LUI 127 containing the domain name. The operations of a U H A provide methods for the U T A to authenticate a user, to update a user's location (machine name or IP address), to get and update the P C E of a user, and to get the profile by application name. A special logout () operation is called by the U T A when the user finishes a session and logs out from the foreign terminal. This allows the U H A to unbind the user from its current location. User terminal agent The U T A object is responsible to handle user requests at the foreign terminal, called by the initial agent in response to user requests. The first operation called is the login() method for authenticating a mobile user. After login, the U T A is responsible for determining an acceptable subset of the user's P C E as supported by the terminal capabilities specified in the terminal profile. It also discovers the locally available facilities by inquiring the local Trader Service when requested by the user. The log in () operation takes a user's LUI and password as parameters. From the domain name part of the LUI, the U T A can determine the location of the U H A by using a directory service. The object reference for the U H A can then be obtained by using the Naming Service as mentioned before. The operation run-app () runs an application. If the application is locally available, the U T A simply runs it locally, with appropriate configurations set for it; otherwise this operation fetches the application and its environment from the U H A and then runs it. The operation should be an asynchronous one, in that the caller (initial agent) can resume operation after the call is issued without waiting for its 128 completion. This allows the initial agent to accept user's input while the application is running. Terminal profile The terminal profile defines the capability of the terminal. This includes the physical capabilities of the screen such as colors, resolution and size, and software capability such as available applications on the terminal (i.e., directly accessible from the terminal). It also includes mapping rules for application configurations. The mapping is typically a matter of copying the configuration files (part of P C E ) , to the local file system where the application will find them. The implementation of this mapping will be dependent on the operating system of the foreign terminal and must be defined and implemented differently for each platform that the U T A runs on. Protocols The U P C system has a number of protocols that support user mobility on the Internet. This includes the middleware support that allows a mobile user to access the network wherever he roams, the mobile user location management protocol, and : mobile user P C E management. We will not detail on the latter two protocols which can be found in the references [64, 63, 93, 94, 110]. The middleware support protocol is the central protocol in U P C which de-scribes the interactions between the user home agent, the terminal initial agent, and the user terminal agent. This protocol provides a virtual global network to the mo-bile user. We choose to use it to demonstrate our test generation approach. In order 129 to make the system more understandable and more manageable, we abstract away some non-essential events, and take the liberty in choosing the representative values for the protocol data parameters, and where non-determinism arises determinizing it appropriately. The abstracted protocol is described as two communicating FSMs in Figure 4.14, where the initial agent and the user terminal agent are combined since the two mostly communicate between themselves. This protocol can be described as a two-CFSM system where N = 2, 51 = {init,regO,regl,reged,update,invoke, getpce}, 52 = {idle, auth, uspreq}, soi = idle, S02 = idle, Moi = {loginO,loginl,runapp, update, logout}, Mio = {prompt, fail}, M11 = {authreqO,authreql,USPreq,PCEreq,updreq,disreq}, M21 = {authrspO,authrsp\,U SPrsp, PCErsp,updrsp,disrsp}, A(init, loginO) = regO, A(init,loginO) = authreqO, A(idle, authreqO) = idle, A(idle, authreqO) = fail, etc. Basically, the protocol works as follows. When a user gets hold of a foreign terminal supporting U P C , he logs into the terminal with loginO or loginl, where loginO represents a failed attempt, e.g., with wrong user name or password, and loginl a correct one. The IA/TJTA, upon receiving this login information, sends it to the home agent for verification (via authreqO or authreql). If the verification succeeds, the I A / U T A is ready to accept user's request to run an application and/or update his P C E . The runapp request works by first requesting a user profile (USPreq) 130 (a) Initial Agent + User Terminal Agent (Ml) updreq/updrsp (b) User Home Agent (M2) (c) The Composite System (M3=MloM2) Figure 4.14: U P C middleware protocol 131 that gives the user's service profile indicating whether the application is local or remote. If it is remote, the I A / U T A proceeds to retrieve the P C E (PCEreq). It then runs the application and returns a prompt after it finishes. Many things are involved in this procedure such as encryption of the user information during authentication, processing of local and remote services, different prompts for different requests, etc., but we abstract away those non-essential details in the C F S M representation. For demonstrating our embedded testing strategy, we consider the case where the home agent is an embedded module. This corresponds to the situation where a mobile user roams to a foreign location, and wishes to access his personal P C E from there. The user has no direct access to the home agent; what he directly interacts with is the initial agent and the terminal agent. The testing issue is therefore how one can test the functionality of the home agent from the viewpoint of a mobile user. We composed the initial agent, the terminal agent, and the home agent to produce a composite system (also shown in Figure 4.14). This global system models the system behavior that a tester can observe and control. 4.7.2 U P C Test suite evaluation Test suite for embedded modules can be generated using methods such as that presented in [77]. However since no tool is available for the method as far as we know, we chose to evaluate a test suite directly generated from the composite system. We use the TJIO-method for this purpose, to get an idea on how the method fares for embedded module testing. The composite machine is completed first, with the assumption that for unspecified transitions, the machine outputs a null output and stays in the same state. It is easy to verify that login 1/prompt is a UIO sequence 132 for state idle, and logout/prompt is a UIO sequence for state logged. This leads to the following test suite: TS = { r/- loginO/fail loginl/prompt r/- runapp/null loginl/prompt r/- update/null loginl/prompt r/- logout/null loginl/prompt r/- loginl/prompt loginO/null logout/prompt r/- loginl/prompt loginl/null logout/prompt r/- loginl/prompt runapp/prompt logout/prompt r/- loginl/prompt update/prompt logout/prompt r/- loginl/prompt logout/prompt loginl/prompt } Feeding this to our tool E C O V , a test tree was yielded as shown in Figure 4.15. It represents a test suite for the U H A as follows: TS = { r/- aureqO/aurspO aureql/aurspl r/- aureql/aurspl USPreq/USPrsp PCEreq/PCErsp disreq/disrsp r/- aureql/aurspl updreq/updrsp disreq/disrsp r/- aureql/aurspl disreq/disrsp aureql/aurspl > This tree is then collapsed using the tool C O V , and the resulting FSMs are composed with the context machine I A / U T A to determine the conformance in 133 134 context. We did some experiments regarding the upper boundary n on number of states for the solution machines (mutants of the U H A machine). For n = 3, there were 4031 solutions, 4026 of which are not conforming; for n = 2, there were 196 solutions, with 192 non-conforming. In the extreme case where n = 1, we get a unique conforming solution with only one state (Figure 4.15). This indicates that the smallest implementation of the U H A can be only one-state, assuming that the test context I A / U T A is correctly implemented. Examining the I A / U T A machine, we can see that if I A / U T A is correct, the state information regarding login, logout, and P C E retrieval would be correctly kept at I A / U T A , and the U H A would not need to store this information, resulting the one-state implementation. In the next chapter, we will move on to the realm of metric space based test coverage measure that targets on behavior coverage instead of fault coverage. Together, they represent our efforts in developing objective and useful coverage measures for protocol testing. 135 Chapter 5 A generalized metric based behavior coverage measure This chapter presents our result on behavior coverage testing, as a complement to fault based testing. As generally recognized, behavior coverage testing is an effective testing technique that can be performed to exercise the behavior space, typically after functional testing in a test campaign. It is less demanding than fault based methods in generating test cases, and provides good confidence in software reliability [42]. A good example of coverage testing in protocol conformance testing is the canonical tester based on the LTS model [10], which attempts to exercise all traces of a specification. However, the tester is infinite for a specification with infinite behavior. In practice, testing must be finished within finite time, therefore an infinite tester has to be truncated. The basic metric-based (MB) method [100, 22] is an effort that endeavors to approximate the infinite space with a finite test suite. Since the basic M B method cannot handle the data portion in a protocol, 136 we aim at extending the basic metric-based method to handle the protocol data [111]. The importance of data storage in real life protocols and their testing can be seen from the numerous research reports on testing data flows in a protocol [97, 86, 20, 69, 102, 15, 16, 47, 5]. While data storage greatly simplifies the specification of complex systems, it also introduces more difficulties in testing, notably in the coverage of data variations. Our generalized metric space is intended to address this problem. We briefly review the basic metric-based method before going into the details of the generalized metric space. 5.1 Basic metric space The basic metric based method defines a metric space over the behavior space made of execution sequences. A set of finite execution sequences, as approximations of infinite sequences, can be selected based on the metric. Furthermore, a finite number of test suites, which approximates the infinite behavior space, can be generated based on the restriction of test cost. The important property of this approximation process is that the series of test suites can converge to the original specification in the limit. Thus, we have a way to achieve coverage of the specification with an arbitrary degree of precision limited only by the test cost. The metric is built on the concept of testing distance between two execution sequences. The distance satisfies the requirement that the resulting space be a metric space and be totally bounded, so that we have the nice property of finite covers of an infinite space [22]. It should also capture the intuitive requirement of testing relationships between execution sequences, so that a concept of "closeness" of sequences can be understood. This closeness actually represents a notion of testing 137 representativeness: the closer the two sequences, the more likely they'll yield the same test result. Formally, testing distance is defined as [22]: Definit ion 5.1 (Basic testing distance) Let s,t be two (finite or infinite) exe-cution sequences in S, where s = {(ak, afc)}fc=i> and t = {(bki Pk)}k-i> K,L E N U {00}. The testing distance between two execution sequences s and t is defined as max.{K,L} dt(s,t) = 5Z Pkh(s,t) k=l where s , ^ \r<*k ~ rfa I */<** = bk Sk(s,t) = < 1 ifak^bk If s and t are of different lengths then the shorter sequence is padded to match the length of the longer sequence, so that 5k = 1 for all k in the padded tail. Note that in the above definition, p and r are functions satisfying the follow-ing properties: PI {pk}kLi 1S a sequence of positive numbers such that Y^'kLiPk = p < 00 . P2 {rfc}£L0 is an increasing sequence in [0,1] such that l i m ^oo = 1. Put r^ = 1. This definition guarantees that the space (S, dt) is a metric space, and more importantly it is totally bounded and complete [22, 21]. It ensures the existence of finite covers for infinite metric space (S,dt), which is the theoretical foundation for the approximation process and also the test selection algorithm. The coverage measure for a set of test sequences T with respect to a set S is defined as Covs(T) = l-ms(T), 138 where sup{dt(s,T)\s E S\T} mS{T) = v o o n :• ms(T) represents the normalized maximum distance from T to S. A large value of ms{T) implies that T is "farther" from 5, hence a smaller coverage. 5.2 Generalized metric space The basic metric based method handles the protocol control space nicely, with par-ticular considerations of recursion depths. However, in a general protocol behavior space where data flow plays an important role, the omission of the data part limits the applicability of the method to protocols at higher level of abstraction with data part abstracted away. A straightforward method to deal with data part may be to expand a protocol with data to the underlying pure finite transition system, by unrolling the data part into discrete values. However, this will cause the well-known state space explosion problem and is only feasible when the data part is small in number of variables and their value ranges. Moreover, even if this expansion is possible, events with different data values would be treated as totally different events, which makes the testing distance insensitive to data differences. In order to solve this problem and broaden the applicability of the basic M B method, we have aimed at generalizing the metric space so as to accommodate both the control flow and data flow of protocols. The idea is to define one metric which incorporates distance contributions from both the execution sequences and data variations. The protocol space can thus be still considered as one metric space, and with proof of total boundedness and completeness of this space, the convergent 139 test selection process and coverage measure can be naturally extended. Moreover, the test selection process can actually be performed in two steps: first for control sequences, and then for data variations. We show that within our distance definition, these two steps can indeed cover the whole protocol space. We first define the concept of generalized execution sequence in our gener-alized protocol space, G, where control flow and data flow are both present. Each event now has associated data values for its parameters, where values can be of integer or real type. A generalized execution sequence is thus a sequence of observ-able events each of which has its parameters instantiated with certain values within their respective ranges. The range for any value is assumed to be finite, which is reasonable in protocols. For recursive events, the same concise notation as in the basic method is employed. However, if the same event recurses with different data values, we do not consider as recursion depth the number of times that the event is repeated. This is because the events are essentially different when data values are different. To avoid confusion, we distinguish between an event and its name: Definition 5.2 (Event) An event in an execution sequence consists of an event name, and a set of associated data values for its parameters. An event can be represented as e(vi,V2,vn) where e is the event name and v \ , v n are a particular data valuation. The type of the data valuations can be either numeric or alphabetic. In communication protocols, data are typically integers (e.g., sequence number) or strings (e.g., identifiers). Definition 5.3 (Generalized execution sequence) A generalized execution se-quence can be represented as a set of pairs: {{ak{v\,V2, ...,vn),p)}, where ak(vi,v2, ...,v 140 is an event with name ak and data values v\,v2, •-.,wn, and p is the recursion depth of the event. Where ambiguity is not possible, we simply use the term "execution sequence". A generalized execution sequence can be considered as a trace in the extended LTS (ELTS) of the protocol. Al l generalized execution sequences of a protocol constitutes the protocol space G. A generalized execution sequence in G is also called a point in the space G. The testing distance between two generalized execution sequences is defined as follows: Definition 5.4 (Generalized testing distance) Let s,t be two (finite or infi-nite) generalized execution sequences in G, where s — {(ak(uk\, ukm), ak)}k=i> and t = {{bk(vki, ...,vkn), (3k)}%=1, K, L G N U {oo}. The testing distance between s and t is defined as max{K,L} dt(s,t)= pk6k(s,t) k=i where a-rdk+p- |rQ f c - rpk \ if ak = bk where a, (i, 7 are constants satisfying: a , / ? > 0 ; 7 > 0 ; 7 > (a + /3)/2; and rdk is the vector distance between two events of the same name: m r d k = r ( J 2 \ u h i - v k i \ ) . i - l The definition of rdk deserves a special mention in the case where the data values are alphabetic or structured. Suppose the ith data value is of a general string type, i.e., Uki = P1V2 •••Pk, Vki = 9i92 • • • qk'• 141 where Pk,Qk' a r e string elements and each has an integer value (say ASCII code for an alphanumerical element, and 0 or 1 for a bit element). Their distance can be defined as: min{fc,fc'} \uki-vki\= \Pj ~Qj\ + \k ~ k'l which is further used in the definition of r ^ . The distance for structured data values, such as a record, a set, or a sequence, can be recursively computed as the sum of each component element. In the definition of dt(s, t), the functions p and r satisfy the same properties as in the basic metric based method. If s, t differ in length, the shorter one will be padded with a null event and Sk = 7 for the padded part. We now prove that the pair (G, dt) is a metric space. Definition 5.5 (Metr ic space) A metric space is a pair (M.d) with M a non-empty set and d a mapping (a metric or distance) of M x M onto the set of non-negative real numbers, that satisfies the following properties: 1. Vx, y € M , d(x, y) = 0 <=> x = y; 2. Vs, y £ M, d{x, y) = d{y, x); 3. Vx, y,z 6 M, d(x, y) < d(x, z) + d(z, y). T h e o r e m 5.1 The pair (G,dt) is a metric space. Proof. It suffices to show that dt is a distance in G. 1. dt(s,t) is a non-negative real number for any s,t. This is straightforward from the fact that Sk is up-bounded by max{a:+/3,7}, and the sequence pk converges. 142 2. dt(s,t) = 0 iff s = t. This can be easily seen from the fact that dt(s,t) = 0 iff Sk(s,t) = 0 for all k, which is equivalent to K = L,ak — bk,uki = vki for all i, and ak = /3k, for all k = 1,2,...,K = L. 3. dt(s,t) = dt(t,s). This directly comes from the fact that 5k{s,t) is symmetric, i.e. 5(s,t) = 6(t,s). 4. dt(s,t) satisfies the triangular inequality. Let s,t,u be three execution sequences in G, u = {{ck{wki, •••,u)ki),jk)}kLi-Without loss of generality, consider the following cases at Sk: Case I: s,t,u all have the same event, i.e. ak = bk = ck. We have 6k{s,u) + 5k(u,t) = {a-rdk{s,u)+(3-\rak - r 7 J ) + (a • rdk (u, t) + j3 • \rlk - r^J) = a • (rdk(s,u) + rdk(u,t))+/3- (|rQjb - r 7 J + \rlk - r 0 k \ ) > ct-rdk(s,t)+ j3-\rQk-rpk\ = Sk(s,t). The inequality rdk(s,u) + rdk(u,t) > rdk(s,t) holds due to a special case of the Minkowski's inequality [46] and also the fact that the function r is increasing. Case II: s,t have the same event, but u's event is different, i.e., ak = bk ^ ck. Since 7 > (a + /3)/2, it follows that Sk(s,u) + 8k(u,t) = 27 > a + p > a • rdk + (3 • \rak - rpj 143 Case III: s,t have different event, but u has the same event as s, i.e., ak = Ck^bk- We have Sk(s,u) + 6k{u,t) = (a • rdk(s,u) + /3 • |r Q A ; - r 7 J ) + 7 > 7 = £ f c ( s , f ) . Case IV: s,t, u all have different event, i.e. ai-,bk,Ck are all different. Obvi-ously, h(s,u) +Sk(u,t) = 7 + 7 > 7 = <5fe(s,t). Therefore, in all cases, we have 8k(s,u) + 5k{u,t) > 6k{s,t), which leads to: max{K,L} max{L,M} dt(s,u) + dt(u,t) = 5Z Pk$k(s,u)+ ]T pk5k{u,t) fe=l fe=l max{K,L} > 5Z Pk8k(s,t) = dt(s,t). k=i • 5.2.1 Interpretat ion of the distance We now give an intuitive interpretation of the testing distance. Same as in the basic M B method, the sequence {pjt}^_1 gives the weight to the difference of two events at each position k. The requirement of pk being convergent implies that the weight should be decreasing with the increase of the length of a sequence. This is consistent with our intuition that the farther a sequence goes, the less significant the difference should be, i.e., that difference contributes less to the testing distance. Of course, one can choose to have different weights for finite number of leading events, but after that point, the weights must converge in a decreasing order. For example, a 144 typical function pk is pk = l/ak(a > 1). One may also define a pk as 1 if 0 < k < 10 Pk = < { l/ak if k > 10 The function 8k measures the difference in recursion depths and data varia-tions. The purpose of using rk in 8k is to normalize the distance contributions, rk is restricted in [0,1] and must be increasing so that dt is a distance in G. For example, we can choose We also use the constants a, (3 and 7 as "fine-tuning" parameters in determining the relative importance of the difference in recursion depths, data variations, and events. As a rule of thumb, we can fine-tune the parameters as follows. 1. If difference in data variations (r<ffc) is considered as more (or same, less) important than that in recursion depths (|rQ f c — rpk\), choose a,/3 such that a > (3 (or a = (3, a < f3, respectively). 2. If difference in events is considered more (or same, less) important than that in recursion depths and data variations, choose a, /?, 7 such that 7 > a + (3 (or 7 = a + (3, (a + (3)/2 < 7 < a + /3, respectively). In the simplest case, we can choose a — (3 = 7 = 1, indicating the same importance of differences in recursion depths, data variations, and actions. If we choose to neglect the data part, i.e., a = 0, and choose f} = 7 = 1, we get ak where a > 0. nt = ak +.1 Sk{s,t) = < rak~rpk\ Hak = bk 1 if ak # bk which is exactly the basic metric space! 145 5.2.2 Example Let a(x, y), b(z, w),c(x, w),d(y, z) be events, where x, y, z are integers, and w a char-acter string. Consider the following three test cases: 1. A = {(a(x, y), 3), (d(y, z),2), (b(z, w),l), }. 2 . 5 = {(a(x,y),2), (c{x,to),2), (b{z, w),2), {c{x, w), 1)}. 3. C = {(b(z,w),2),(c(x,w),3),(d(y,z),l),{c(x,w),2)}. Using the generalized testing distance in Definition 5.4 with the following parameters: Pk = \ and 2 if 1 < k < 2 l / 2 f c - 2 if >fc > 2 k rk = ——, a = 13 = 1, 7 = 2. k + 1 Suppose in test case A , x = 1, y = 2, z = 3, to = "DataStringl", in B, x = 4,y = 3,z = 9,w = "AnotherData", and in C, x = 8,y = 6,z = 5, to = "GoodTests!", we have £ r ( A , B) = rdl + | r Q l - | = r(3 + l) + | r (3) -r (2) | = 0.883, = 2, <53(A,B) = rd3 + \ra3 - rp3\ = r(6 + 173) + | r ( l ) - r ( 2 ) | 146 = 1.161, 84(A,B) = 2. Therefore the testing distance between A and B is: 4 dt(A,B) = YtPkSk = 7.927. Similarly, we can calculate dt{A,C) = 11, dt(B,C) = 7.119. What this means is that, among the three test cases, B and C are the closest while A and C are the farthest. If we draw a picture with A,B and C as points in the protocol behavior space, they would appear as a triangle as in Figure 5.1. Figure 5.1: Testing distance between test cases A , B, and C 5.3 Total boundedness and completeness In order to be able to use finite test suite to approximate the specification (infinite number of execution sequences) with arbitrary degree of precision, we must show that the generalized metric space (G, dt) is totally bounded and complete, as is the case in the basic M B method. 147 Definition 5.6 (Total boundedness) A metric space S is totally bounded if for every e > 0 it is possible to cover S by a finite number of spheres with radius e. T h e o r e m 5.2 The generalized metric space (G, dt) is totally bounded. Proof. Suppose e is an arbitrary positive number. Let YlkLi Pk — P and ke be such that Y^T=ke+iPk < e/27- Let ne be such that for all k > n€, rk > 1 — n, where n = e/2p/3. E is the set of all events with data valuations. Since we assume finite value range of data parameters, E is finite. Therefore, the set F = {{(ai(vn, ...,Vin),ai)}kLi\ai(viU •••,vin) € E,ai€ {1, ...,ne}} is finite. We claim that the set of all spheres of radius e centered at elements of F covers the entire space. To see this, let s = {(bi(un,Uin), Pi)}f=l be arbitrary. Then there exists t = {ai(vn,V{n), cti)\kLl in F such that a, = bi and Uij = Vij for i = 1 , k e and j = 1 , n . Make OJJ = if 0i < ne or ai = n£ if > n £ . Note that with this choice of t, rdk(s,t) = 0 for i = l,...,ke. We have max{fc£,L} dt{s,t) = 51 PkSk(s,t) k=l kc OO < ^2Pk(a-rdk +P- \rak -rpk\) + 7 " Yl Pk k=l k=kc+l ke oo < J2pk{/3-\rne-l\)+l- £ Pk k-l k=ke+l < p • (3n + 7 • e /27 < e/2 + e/2 = e. This completes our proof of the theorem. • 148 Total boundedness is very important for the subsequent test selection because it implies the existence of finite number of balls of radius e that covers the metric space. This makes it possible to choose finite number of test sequences (points in G), each belonging to one ball, to cover the protocol behavior space. The points that fall into a particular ball are all represented by the chosen point (a test sequence) in the sense that their testing distances are small enough. The total boundedness property itself is not enough for test selection, since we want to choose test sequences incrementally, and eventually, the protocol space will be fully covered. This relies on the completeness property that we now proceed to prove. In general, we want the metric space to be compact, i.e. both totally bounded and complete. To prove the compactness of the metric space (G,dt), we need to use the following definition and proposition: Definit ion 5.7 (Completeness) A metric space is complete if every Cauchy se-quence in it is convergent to a point of the space. Propos i t ion 5.1 [84]: A metric space is compact if and only if it is complete and totally bounded. As we have proved the boundedness of (G,dt), we now only need to prove the completeness of (G,dt), i.e. every Cauchy sequence in G converges to a point in G. T h e o r e m 5.3 The generalized metric space (G, dt) is complete. Proof. Let {gn}%Li be a Cauchy sequence in G, where gn = {(a\n\v^\ ...,t>^), ot(il)))i=\\ K { n ) e N U {oo}. By definition, Ve > 0 3N£ [Vm, n> Ne ^ dt{gm, gn) < e] 149 where Ne,m,n 6 N . Let k be arbitrary. We first show that liTarrijn^>.00dk(gm,gn) = 0. For an arbitrary 77 > 0, choose e such that e < rjpk. By definition, there exists Ne such that dt(gm,gn) < e for all m,n> Ne. Therefore Pkfa{9m,9n) < dt{gm,gn) <e< rjpk. Consequently, Sk(gm,gn) < 77 for all m,n > Ne. This proves l i n i m ^ o o Sk(gm, gn) = 0. By the definition of 6k, we can conclude that the sequence {K^}^=1 must converge to K, K € N U {00}. To see this, consider two cases: a) are all finite, then must be eventually constant, i.e., equals K, K 6 N , since otherwise 5k{9m,9n) > 7 and cannot converge to 0; b) —>• 00 when n —> 00, in which case we also conveniently say converges to 00. Similarly, we can conclude that lim rd = 0 and lim \rak-rg,\=0. m,n—>oo " m,n—•(» This implies that the sequences {a^}™^, {u , -^}£Li 's , and {af^}^} are all conver-gent. Let Ui(vn, ...,vik) = limn^00aln\vli\...,v$) and a; = l i m ^ o o af1^. Since i is arbitrary, we get the sequence g = {(ai(vn, ...,Vik), c t i ) } f = l , K G N U {00}, which is a point in space G. We claim that the sequence {gn}^Li converges to g. This is obvious when K is finite since eventually gn = g. To prove the case where K = 00, let e > 0 be arbitrary. Choose k£ such that YlTe+iPk < e /2- Since l imn-^oo Sk(gn,g) = 0, we can choose ne such that 5k(gn,g) < e/2p (where p = X ^ i P f c ) f ° r all 1 < A; < fce and for all n > n£. Therefore, for all n > ne we have 00 dt(gn,g) = J2Pksk(9n,g) k=l 150 < k=\ k=kt+l < < This proves that the Cauchy sequence {gn}^Li in G converges to a point in G with respect to dt, therefore (G,dt) is complete.• From Theorem 5.2 and 5.3 and the Proposition, we obtain the following compactness theorem. T h e o r e m 5.4 The generalized metric space (G,dt) is compact.O The compactness (i.e., total boundedness plus completeness) lays the foun-dation of test selection and coverage measure in the next section. We will modify the test selection process in the basic M B method to make it applicable to the generalized space. 5.4 G e n e r a l i z e d c o v e r a g e m e a s u r e a n d tes t s e l e c t i o n The basic idea in test selection with the basic M B method is to generate e-dense1 set of test sequences with respect to the protocol specification or some original test suite. By choosing e arbitrarily small and incrementally adding more test sequences, we can achieve arbitrary accuracy in covering the protocol specification in a convergent manner. 1A set T is said to be e-dense (e > 0) in a set 5 if for every s € S there is t 6 T such that dt(s,t) < e. 151 We adopt the same idea in our generalized metric space, with extensions to handle, the data valuations. For simplicity, we omit the cost factor [100] in our algorithm, and focus on the selection of e-dense test suites with respect to a set of execution sequences which can be finite or infinite. A l g o r i t h m 5.1 Selection of an e-dense set of test sequences Input: G: original set of execution sequences, e: density requirement. Output: T: selected e-dense set of test sequences. Step 1: Initially, T = cp (empty). Also let X = G. Step 2: If X = cp return T and exit. Otherwise randomly remove a test sequence t from X (i.e. X <— X — {t}), apply appropriate data valuations where data are involved, and calculate dt(t,T). Step 3: Ifdt(t,T) > e, T <- T U {*}. Go to Step 2. Using the same idea of multi-pass algorithm with decreasing e density, we obtain a set of Cauchy sequences over the successive passes. These Cauchy sequences converge to infinite execution sequences in the specification when G is infinite. Since the space (G, dt) is totally bounded, we can eventually find the finite covering of G with density e, at which point the algorithm terminates. It is also worthwhile to note that in Step 2 when data valuations are gener-ated, we can either simply generate random data values, or intentionally select fault sensitive data values such as boundary values and typical values. In this way, some test data generation criteria that have been proved effective in software testing can be incorporated. In practice, we need also consider the executability of an execution sequence. This executability checking can be performed on-the-fly as data values are chosen, using the method in [16] or [47]. 152 In the implementation of the algorithm, we may also consider all data vari-ations for an execution sequence before proceeding to a new execution sequence, or consider all execution sequences with distinct control part before embarking on data variations. Either way we can have a more clear-cut two pass algorithm that clearly distinguishes between the control and data part, and yet they together cover the whole protocol space with a desired test suite density. From the test selection process, we can actually measure the coverage of a test suite with density e. This can be seen by observing that sup{dt(g, T) : g € G\T} < e Using the same definition of the basic M B method, we have sup{dt(g,T) :g£G\T} e mcKT) = =^5 < - , Efc=iPfc P where p = E/£LiPfc- Consequently, CovG{T) = 1 - mG(T) > 1 - - . P Using 1 — e/p as the coverage of T with respect to G would be a fair measure since it is the lower bound of the exact coverage. The property lime_>o COVQ (T) = 1 also indicates that with arbitrarily small e density, the test suite can ultimately cover the whole space. 5.5 Discussion The problem of test generation and selection that can handle both the control and data parts of protocols has been considered as a difficult practical problem for which no tractable analytical solution has been found. We have presented a generalization 153 of the basic metric based test selection method where both the control and data parts of protocols can be handled. The major contributions include a generalized metric space definition, the proof of total boundedness and completeness properties of the space, and a generalized test selection algorithm. This lays out a metric based testing framework where extended protocol space can be tackled. In our generalized test selection algorithm, it is also possible to incorporate test data generation criteria that have been proved effective in discovering program faults, such as boundary values, typical values, and values that cover data dependencies, etc. This could be a point where our metric based method is joined by the traditional software testing techniques, and therefore its effectiveness and applicability are boosted. It is true that the M B method critically hinges on the definition of testing distance, and with different definitions, the effectiveness may be different. However, the testing distance is intended to provide a way to measure the "closeness" or "rep-resentativeness" of test sequences. The exact meaning of the "closeness" concept relies on our experience and expertise in protocol testing. With our definition of the testing distance, we believe many important protocol properties, such as recursion, concurrency, and data variations, are already captured in the definition. With ap-propriate parameterization of the functions r and p, and the fine-tuning constants a, (3 and 7, a "good" testing distance definition which reflects our experiences in protocol testing is possible. It is of course a non-trivial task to incorporate expert knowledge into the parameters. This is actually a further research area where heuris-tics need to be developed to provide guidance to the choice of metric functions and parameterizations. A n initial research work that evaluates the sensitivity of metric functions to recursion depths, concurrent connections, and transition patterns is reported in [23]. 154 Chapter 6 Conclusions We have presented our work on coverage measures for both fault based testing and metric based testing. A major difficulty in testing complex systems, especially com-munication protocols, lies in the lack of formal objective measures of test coverage. We have tried to shed some light in this direction by developing formal coverage mea-sures based on fault models and coverage metrics, and applying them to practical protocols. We summarize the work presented and the contributions made by the thesis in the next section, followed by a section on some possible future work along this direction. 6.1 Contributions The central thesis that we defend is that our fault based coverage measure can contribute a basis for practical communication protocol testing, which offers the important advantages of independence of specific fault classes, accurate coverage measure calculation, and amenability to incremental test suite generation based 155 on coverage requirement and fault localization. We also explored a test coverage measure based on behavior coverage. This latter measure lends itself in handling protocols with large data space, which would have been difficult to analyze with fault based methods due to the large state space and complex fault models. The main contributions of this thesis are as follows. 6.1.1 Fault coverage measure Traditional fault coverage analysis is based on fault simulation with explicit fault models. This approach, while very useful in practice, lacks the robustness and accuracy that are needed in many cases, such as in the case of a critical protocol software. We formulated a fault coverage measure that is based on faulty machine identification. Instead of enumerating fault models and randomly generating mutant machines, we try to generate only those machines that can pass a test suite but fails to conform to the specification. The calculation of such a measure is a difficult problem; in fact it is in general NP-complete to find a machine that satisfies a given behavior sample (test suite in our case). We successfully applied search optimization techniques developed in AI, prominently domain reduction (static pruning) and backjumping (dynamic pruning), to the problem. This has effectively improved the performance of the algorithm, which is shown by a successful application of our tool to three real life protocols, i.e., ISDN BRI protocol, T C P connection management protocol, and the NBS Transport Class 4 protocol, whose complexities are rather typical in communications protocols, and perhaps are more complex in control part than most protocols in use today. 156 6.1.2 Incremental test generation and fault localization We have explored the application of our coverage measure to test suite generation and fault localization. While it is unclear whether the test enhancement approach is better than generating a complete test suite in the first place using methods such as DS and W methods, our technique does allow an incremental generation of test cases based on coverage requirement, thereby offering more flexibility in test generation where test suites with increasing test coverage are needed. Fault localization based on the measure also provides a useful diagnosis tool for test result analysis. The coverage measure also allows an evaluation of test sequence optimization techniques, an active research effort in reducing cost while maintaining test cover-age. Our findings show that although optimizations intend to maintain coverage, they usually cannot have both birds in hand. Of the optimization techniques that we evaluated, coverage is invariably weakened in proportion to the amount of op-timization. While this conclusion may not be general, it shows that strict proof of coverage preservation is needed when doing optimization, and excessive optimization may not be desirable. 6.1.3 Embedded testing fault coverage Embedded testing has been a difficult problem due to the limited controllability and observability of the embedded module. Research has been conducted in test generation; however little work has been done toward test coverage evaluation. We studied this problem and extended the coverage measure that was developed for single machine testing to embedded testing. This translated essentially into a test tree generation problem, since the tree can be collapsed using the approach in the single machine test evaluation. We presented the algorithms for test tree generation 157 and determination of conformance in context, and implemented them in a tool set called ECOV. The tools are applied to an example and demonstrates the concept and approach of our coverage measure. We also proved that the problem of deciding if there is an embedded FSM satisfying a given (composite) system behavior within certain test context is in general NP-complete. This indicates that the coverage calculation is in general a hard problem, but with search optimization techniques, it can be solved with efficiency in many cases. 6.1.4 Testing of a universal personal computing protocol We described a universal personal computing (UPC) system, which the author as a member of a team has contributed to the design, prototyping, and testing. UPC is a powerful system that allows personal mobility on the Internet. It is a service-oriented mobility support with or without host mobility support (which is typically supported by mobile IP). The idea of moving a user's computing environment to where the user currently connects to the Internet offers a truly virtual global service network. We modeled one of the key UPC protocol, i.e., the middleware part, as a CFSM system consisting of three communicating components, and use it as a guinea pig for our embedded testing coverage measure in the context of multiple modules. Test cases were generated and analyzed with our tool ECOV, and a smallest possible implementation for the embedded module was found as a result. This demonstrates the applicability of our coverage measure to real life protocols. 158 6.1.5 Generalized coverage metric The previous contributions have been targeted on fault based testing. This last contribution, however, deals with the coverage issue in an entirely different setting: coverage based on a metric space with testing distance metrics. This approach aims at behavior coverage without concerning fault models. The objective is to cover the behavior space under the testing distance metrics, possibly with an incremental approach that produces incrementally improved test cases. Our contribution is in the extension of the existing basic metric space, which can only handle the control flow of a protocol, to a generalized metric space that can handle both the control and data flow in a protocol. We proposed the definition of such a generalized metric space while avoiding simply unfolding the data values (which would not work for large data spaces). This generalized metric space not only inherits the properties of the basic metric space, i.e., integration of recursion and concurrency, but also allows flexible data value selection that have been developed in software testing such as boundary values, typical values, and data dependencies. We also proved that the generalized metric space preserved the total bound-edness and completeness properties, which allows a convergent test selection process. Although the number of test cases may grow exponentially with respect to the test density, the test selection offers an approach that can produce test cases of arbitrary coverage. Testers can then determine what a coverage is satisfactory based on other constraints such as testing time and budget, and select test cases accordingly. 159 6.2 Future work We have identified some possible future research that may improve the work pre-sented in this thesis. Further improvement of the coverage measure calculation While the performance of our tool C O V has been improved with search optimization techniques, we feel there are still room for further improvement. One of the tech-niques is learning while searching, which records useful information obtained during search, which can be used later in pruning the search space [25]. This information can be considered as implicit constraints which are made explicit during the search process. The idea of so-called "controlled learning" is particularly attractive, which learns the new constraints when dead-ends are encountered. At the dead-end, the current set of instantiations is called a conflict set. The key idea is to find one or more subsets of the conflict set and record them, so that in the future exploration of the search space, they may be used to avoid a futile search that contains this conflict subset. The price for this kind of pruning is that we need extra storage to record the conflict set. In the worst case, the space requirement is exponential to the cardinality of the conflict set. This price may be paid off for large problems now that memory prices have dropped dramatically in the last couple of years. In the case of embedded testing, the tool may be optimized by directly col-lapsing the test trees during construction. Currently, the trees generated by E C O V are exported to a file, which is read in by C O V for collapsing the trees. 160 More empirical results While we have demonstrated our approach with tools and real examples, it would be interesting to do more experiments in two aspects: 1. Embedded testing: Recently development of embedded systems on the Inter-net has captured significant attentions [51]. It is practically important to see if those embedded systems can be tested with an embedded testing architecture. Internet provides a wide range of testbeds for distributed computing with many types of embedded systems, such as routers, Internet phones, NetTVs, WebTV set-top boxes, and so on. Modeling such a system (with its environments) as communicating finite machines and applying our testing methodology would contribute a lot to the reliability of the systems. 2. General metric space: A n application of the metric space to real protocols should be more revealing in the usefulness of this theoretically sound approach. A tool needs to be built and integrated into a F D T tool set. The study of integrating data value selection techniques developed in software testing should also take place in order to explore ways to incorporate those criteria into the test distance definition. Fault coverage of the behavior coverage metric The relationship between the metric based coverage and fault coverage is an interest-ing issue. As fault coverage is the only recognized ultimate criterion for evaluating any test method, the metric based behavior coverage would have to show that it is effective in detecting faults to gain more acceptance from the protocol testing community. The idea of integrating fault detecting capability into the definition of 161 testing distance is appealing theoretically, but it has to be shown how this can be done in practice. The current definition of the testing distance captures some impor-tant protocol properties such as recursion and data variations, and serves to prove the total boundedness property of the behavior space. However it is not sufficient for embodying fault detecting properties and it is unclear how these properties can be quantified and parameterized. Moreover, we need to show that the behavior space remains totally bounded with the new parameters for fault detecting capability. Research never ends. 162 Bibliography [1] S. Abramsky. Observation equivalence as a testing equivalence. Theoretical Computer Science, 53:225-241, 1987. [2] A . V . Aho, A . T . Dahbura, D. Lee, and M . U . Uyar. A n optimization tech-nique for protocol conformance test generation based on UIO sequences and rural Chinese postman tours. IEEE Transactions on Communications, 39(11), November 1991. [3] A . V . Aho, J . E . Hopcroft, and J.D. Ullman. The Design and Analysis of Com-puter Algorithms. Addison-Wesley Publishing Company, 1974. [4] A . V . Aho, R. Sethi, and J.D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley Publishing Company, 1986. [5] A . F . Ates and B. Sarikaya. Test sequence generation and timed testing. Com-puter Networks and ISDN Systems, 29:107-131, 1996. [6] Boris Beizer. Software Testing Techniques, 2nd Edition. Van Nostrand Rein-hold, New York, 1990. [7] G.v. Bochmann and C A . Sunshine. A survey of formal methods. In P .E. Green, editor, Computer Networks and Protocols. Plenum Press, 1983. [8] T . Bolognesi and E . Brinksma. Introduction to the ISO specification language L O T O S . Computer Networks and ISDN Systems, 14:25-59, 1987. [9] D. Brand and P. Zafiropulo. On communicating finite state machines. Journal of the Association for Computing Machinery, 30(2), April 1983. [10] E . Brinksma. A theory for the derivation of tests. In Protocol Specification, Testing and Verification VIII. North-Holland, Amsterdam, 1988. [11] T . A . Budd. Mutation analysis: Ideas, examples, problems and prospects. In B. Chandrasekran and S. Radicchi, editors, Computer Program Testing. North-holland, 1981. 163 s [12] T . A . Budd and D. Angluin. Two notions of correctness and their relation to testing. Acta Informatica, 18(1), 1982. [13] A.R. Cavalli and S.U. Kim. Automated protocol conformance test generation based on formal methods for L O T O S specifications. In IFIP 5th Int. Workshop on Protocol Test Systems, pages 212-220, 1992. [14] C C I T T Red Book, vol.III. FASCICLE III.5 - Integrated Services Digital Net-work (ISDN) Recommendations (Study Group XVIII). 1984. [15] S.T. Chanson and J . Zhu. A unified approach to protocol test sequence gen-eration. In Proc. IEEE INFOCOM, San Francisco, March 1993. [16] S.T. Chanson and J . Zhu. Automatic protocol test suite derivation. In Proc. IEEE INFOCOM, Toronto, Canada, June 1994. [17] M.S. Chen, Y . Choi, and A. Kershenbaum. Approaches utilizing segment overlap to minimize test sequences. In Proc. IFIP 10th Int. Symp. on Protocol Specification, Testing, and Verification, 1990. [18] J . C . Cherniavsky and O H . Smith. A theory of program testing with applica-tions. In Proc. Workshop on Softw. Testing, 1986. [19] T.S. Chow. Testing software design modeled by finite-state machines. IEEE Transactions on Software Engineering, May 1978. [20] A . Chung and D. Sidhu. Fault coverage of probabilistic test sequence. In Proc. IWTCS'90, November 1990. [21] J .A. Curgus. A metric based theory of test selection and coverage for commu-nication protocols. PhD thesis, Dept. of Computer Science, Univ. of British Columbia, June 1993. [22] J .A . Curgus and S.T. Vuong. A metric based theory of test selection and coverage. In Proc. IFIP 13th Symp. Protocol Specification, Testing, and Ver-ification, May 1993. [23] J .A. Curgus, S.T. Vuong, and J . Zhu. Sensitivity analysis of the metric based test selection. In IFIP 10th Int. Workshop on Testing of Communicating Systems, Cheju Island, Korea, September 1997. [24] A . Dahbura and K . Sabnani. A n experience in estimating fault coverage of a protocol test. In Proc. IEEE INFOCOM, 1988. [25] R. Dechter. Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition. Artificial Intelligence, 41(3):273-312, 1990. 164 R.A. DeMillo, R .J . Lipton, and F . G . Sayward. Hints on test data selection. IEEE Computer, C - l l , April 1978. R.A. DeMillo and A . J . Offutt. Constraint-based automatic test data genera-tion. IEEE Transactions on Software Engineering, 17(9), September 1991. J.W. Duran and S.C. Ntafos. A n evaluation of random testing. IEEE Trans-actions on Software Engineering, November 1984. C. Perkins (ed). IP Mobility Support; RFC-2002. Internet Requests for Com-ments, (2002), October 1996. J . Postel (ed). Transmission Control Protocol; RFC-793. Internet Requests for Comments, (793), September 1981. E . Brinksma et al. L O T O S specifications, their implementations and their tests. In Proc. IFIP 6th Int. Symp on Protocol Specification, Testing, and Verification, 1986. S. Fujiwara et al. Test selection based on finite state models. IEEE Transac-tions on Software Engineering, June 1991. A . D . Friedman and P.R. Menon. Fault Detection in Digital Circuits. Prentice-Hall, Inc., 1971. A. Gill. Introduction to the Theory of Finite State Machines. McGraw-Hill Book Company, Inc., 1962. R.J.van Glabbeek. The linear time-branching time spectrum. In LNCS 458, 1990. E . M . Gold. System identification via state characterization. Automatica, 8:621-636, 1972. E . M . Gold. Complexity of automaton identification from given data. Infor-mation and Control, 37:302-320, 1978. W . G . Golson and W . C . Rounds. Connections between two theories of con-vurrency: Metric spaces and synchronization trees. Information and Control, 57:102-124, 1983. G. Gonenc. A method for the design of fault detection experiments. IEEE Transactions on Computer, June 1970. J.S. Gourlay. A mathematical framework for the investigation of testing. IEEE Transactions on Software Engineering, November 1983. 165 [41] R. Groz, O. Charles, and J. Renevot. Relating conformance test coverage to formal specifications. In R. Gotzhein and J. Bredereke, editors, Proc. FORTE/PSTV'96, Kaiserslautern, Germany, 1996. [42] D. Hamlet. Connecting test coverage to software dependability. In Software, 1994 Symposium, 1994. [43] D. Hamlet. Software quality, software process, and software testing. In M.C. Yovits, editor, Advances in Computers, volume 41. 1995. [44] M . A. Harrison., On asymptotic estimates in switching theory and automata theory. Journal of ACM, 13:151-157, 1966. [45] F.C. Hennie. Fault detecting experiments for sequential circuits. In Proc. 5th Ann. Symp. Switching Theory and Logical Design, pages 95-110, Princeton, N.J., 1964. [46] E. Hewitt and K. Stromberg. Real and Abstract Analysis. Springer-Verlag, 1965. [47] T. Higashino and G.v. Bochmann. Automatic analysis and test case derivation for a restricted class of LOTOS expressions with data parameters. IEEE Transactions on Software Engineering, 20(1), January 1994. [48] C.A.R. Hoare. Communicating Sequentical Processes. Prentice-Hall, 1985. [49] G.J. Holzmann. Design and Validation of Protocols. Prentice-Hall, Inc., 1991. [50] W.E. Howden. Reliability of the path analysis testing strategy. IEEE Trans-actions on Software Engineering, September 1976. [51] IEEE Computer Society. IEEE Internet Computing. July 1998. [52] ISO/IEC 9646. Information Technology - Open Systems Interconnection -Conformance testing methodology and framework. March 1991. [53] Luiz Paula Lima Jr. and Ana R. Cavalli. A pragmatic approach to generating test sequence for embedded systems. In IFIP 10th Int. Workshop on Testing of Communicating Systems, Cheju Island, Korea, September 1997. [54] JTCl/SC21/WGl/Project 54.1. FMCT Guidelines on Test generation Meth-ods from Formal Descriptions. February 1995. [55] JTCl/SC21/WGl/Project 54.1. Framework: Formal Methods in Confor-mance Testing. February 1995. [56] D. Kang, S. Kang, M . Kim, and S. Yoo. A weighted random walk approach for conformance testing of a system specified as communicating finite state machines. In Proc. FORTE/PSTV'97, Osaka, Japan, November 1997. 166 [57] J. Kella. State minimization of incompletely specified sequential machines. IEEE Transactions on Computers, 19(4), April 1970. [58] J . Kella. Sequential machine identification. IEEE Transactions on Computers, 20(3), March 1971. [59] Z. Kohavi. Switching and Finite Automata Theory. New York: McGraw Hill, 1978. [60] G . Leduc. A framework based on implementation relations for implementing L O T O S specifications. Computer Networks and ISDN Systems, 25(1):23-41, 1992. [61] D. Lee, K. Sabnani, D. Kristol, and S. Paul. Conformance testing of protocols specified as communicating finite state machines - A guided random walk based approach. IEEE Trans. Comm., 44(5), May 1993. [62] D. Lee and M . Yannakakis. Testing finite-state machine: State identification and verification. IEEE Transactions on Computers, 43(3):306-320, March 1994. [63] Y . L i and V. Leung. Protocol architecture for universal personal comput-ing. IEEE Journal on Selected Areas in Communications, 15(8):1467-1476, October 1997. [64] Y . L i and V. Leung. Supporting personal mobility for nomadic computing over Internet. ACM Mobile Computing and Communications Review, 1(1):22-31, April 1997. [65] B. Littlewood and L . Strigini. Validation of ultra-high dependability for software-based systems. Comm. ACM, 36(11), November 1993. [66] F . Lombardi and Y . - N . Shen. Evaluation and improvement of fault coverage of conformance testing by UIO sequences. IEEE Transactions on Communi-cations, 40(8), Auguest 1992. [67] G . Luo, G.v. Bochmann, and A. Petrenko. Test selection based on communi-cating nondeterministic finite-state machines using a generalized Wp method. IEEE Transactions on Software Engineering, 20(2), Februry 1994. [68] R . E . Miller and S. Paul. Generating minimal length test sequences for con-formance testing of communication protocols. In Proc. IEEE INFOCOM'91, 1991. [69] R . E . Miller and S. Paul. On generating test sequences for combined control and data flow for conformance testing of communication protocols. In Proc. IFIP 12th Int. Symp. on Protocol Specification, Testing, and Verification, June 1992. 167 R. Milner. A Calculus of Communicating Systems. LNCS 92, Springer-Verlag, 1980. E . F . Moore. Gedanken-experiments on sequential machines. In Automata Studies, pages 129-153. Princeton University Press, 1956. S. Naito and M . Tsunoyama. Fault detection for sequential machines by transition-tours. In Proc. IEEE Fault-Tolerant Computing, 1981. R. De Nicola. Extensional equivalences for transition systems. Acta Informat-ica, 24:211-237, 1987. A . F . Petrenko. Checking experiments with protocol machines. In Proc. 4th Int. Workshop on Protocol Testing System, 1991. A . F . Petrenko, G.v. Bochmann, and R. Dssouli. Conformance relations and test derivation. In Protocol Test Systems, VI, volume C-19, 1994. A . F . Petrenko and N. Yevtushenko. Test suite generation for a F S M with a given type of implementation errors. In Proc. IFIP 12th Symp. Protocol Specification, Testing, and Verification, 1992. A . F . Petrenko and N. Yevtushenko. Fault detection in embedded components. In IFIP 10th Int. Workshop on Testing of Communicating Systems, Cheju Island, Korea, September 1997. A . F . Petrenko, N. Yevtushenko, and G.v. Bochmann. Fault models for testing in context. In Proc. IFIP FORTE IX/PSTV XVI, Kaiserslautern, Germany, October 1996. A . F . Petrenko, N. Yevtushenko, G.v. Bochmann, and R. Dssouli. Testing in context: framework and test derivation. Computer Communications, 19:1236-1249, 1996. D . H . Pitt and D. Freestone. The derivation of conformance tests from L O T O S specification. IEEE Transactions on Software Engineering, 16(12), December 1990. A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In Lecture Notes in Computer Science, Vol 224, pages 510-584, Springer-Verlag, 1986. D. Rayner. OSI conformance testing. Computer Networks and ISDN Systems, 14(1), 1987. F . S. Roberts. Measurement theory. Addison-Wesley, 1979. 168 [84] H . L . Royden. Real Analysis. Macmillan Publishing Company, New York, 1988. [85] K . Sabnani and A. Dahbura. A protocol test generation procedure. Computer Networks and ISDN Systems, 15:285-297, 1988. [86] B. Sarikaya, G.v. Bochmann, and E . Cerny. A test methodology for protocol testing. IEEE Transactions on Software Engineering, May 1987. [87] Y . - N Shen, F . Lombardi, and A . T . Dahbura. Protocol conformance testing using multiple UIO sequences. In Proc. IFIP 9th Int. Symp. on Protocol Specification, Testing, and Verification, 1989. [88] D.P. Sidhu. Protocol testing: The first ten years, the next ten years. In Proc. IFIP 10th Symp. Protocol Specification, Testing, and Verification, 1990. [89] D.P. Sidhu and T.P. Blumer. Verification of NBS Class 4 transport protocol. IEEE Transactions on Software Engineering, pages 781-789, August 1986. [90] D.P. Sidhu and T . - K . Leung. Formal methods for protocol testing: A detailed study. IEEE Transactions on Software Engineering, April 1989. [91] Q . M . Tan, A . Petrenko, and G.v. Bochmann. Modelling basic L O T O S by FSMs for conformance testing. In Protocol Specification, Testing and Verifi-cation, XV, 1995. [92] A.S. Tanenbaum. Computer Networks. Prentice Hall P T R , third edition, 1996. [93] M . Toro, J . Zhu, and V. Leung. SDL specification and verification of universal personal computing with ObjectGEODE. In Proc. FORTE/PSTV'98, Paris, France, November 1998. [94] M . Toro, J . Zhu, Y . L i , and V. Leung. A C O R B A based framework for univer-sal personal computing on the Internet. In Proc. Joint World Multiconference on Systemics, Cybernetics and Informatics (SCI'98) and the 4th Int. Conf. on Information Systems Analysis and Synthesis (ISAS'98), Orlando, USA, July 1998. [95] J . Tretmans. A formal approach to conformance testing. In O. Rafiq, editor, Protocol Test Systems VI, pages 257-276, 1994. [96] J . Tretmans. Conformance testing with labelled transition systems: Implemen-tation relations and test generation. Computer Networks and ISDN Systems, 29:49-79, 1996. [97] H . Ural. Test sequence selection based on static data flow analysis. Computer Communication, 10(5), 1987. 169 [98] F.W. Vaandrager. On the relationship between process algebra and in-put/output automata. In IEEE, pages 387-398, 1991. [99] S.T. Vuong and W.Y.L Chan. The TJIOv-method for protocol test sequence generation. In Proc. 2nd Int. Workshop on Protocol Testing System, October 1989. [100] S.T. Vuong and J.A. Curgus. On test coverage metrics for communication protocols. In Proc. J^th Int. Workshop on Protocol Testing System, 1991. [101] S.T. Vuong and K.C. Ko. A novel approach to protocol test sequence gener-ation. In Proc. GLOBECOM'90, December 1990. [102] C-J Wang and M.T. Liu. Axiomatic test sequence generation for extended finite state machines. In Proc. 12th Int. Conf. on DCS, Yokohama, Japan, June 1992. [103] O H . West. An automated technique of communication protocol validation. IEEE Trans. Comm., 28, 1978. [104] E.J. Weyuker. Can we measure software testing effectiveness? In Software Metrics, 1993 Symposium, pages 100-107, 1993. [105] M. Yannakakis and D. Lee. Testing finite state machines. In 23rd Annual ACM Symposium on Theory of Computing, pages 476-485, Louisiana, 1991. [106] M. Yao, A. Petrenko, and G.v. Bochmann. Fault coverage analysis in respect to an FSM specification. In IEEE Infocom'94, Toronto, Canada, 1994. [107] M. Yao, A. Petrenko, and G.v. Bochmann. A structural analysis approach to the evaluation of fault coverage for protocol conformance testing. In D. Hogrefe and S. Leue, editors, FORTE'94, 1994. [108] J. Zhu and S.T. Chanson. Fault coverage evaluation of protocol test sequences. Technical Report 93-19, Dept of Computer Science, Univ of British Columbia, June 1993. [109] J. Zhu and S.T. Chanson. Toward evaluating fault coverage of protocol test sequences. In Proc. IFIP 14th Int. Symp. on Protocol Specification, Testing, and Verification, Vancouver, Canada, June 1994. [110] J. Zhu, M. Toro, V. Leung, and S. Vuong. Supporting universal personal computing on the Internet with Java and CORBA. Concurrency: Practice and Experience, 10(1), 1998. [Ill] J. Zhu and S.T. Vuong. Generalized metric based test selection and coverage measure for communication protocols. In FORTE/PSTV'97, Osaka, Japan, November 1997. 170 [112] J . Zhu, S.T. Vuong, and S.T. Chanson. Evaluation of test coverage for em-bedded system testing. In Proc. IWTCS'98, Tomsk, Russia, September 1998. 171 Appendix A UIO-based Test Sequences for BRI r/- UIl?setupbad/UIl!relcom UI17setupbad/UIlIrelcom r/- UIl?info/- UIl?setupbad/UIl!relcom r/- UIl?infobad/- UIl?setupbad/UIlIrelcom r/- UIl?infolast/- UIl?setupbad/UIlIrelcom r/- UIl?rel/UIlIrelcom UIl?setupbad/UIlIrelcom r/- UIl?disc/- UIl?setupbad/UIlIrelcom r/- T302?timeout/- UIl?setupbad/UIlIrelcom r/- NI2?netclear/- UIl?setupbad/UIlIrelcom r/- NI2?netalert/- UIl?setupbad/UIlIrelcom r/- NI2?netconn/- UIl?setupbad/UIlIrelcom r/- UIlTconnack/- UIl?setupbad/UIlIrelcom r/- T305?timeout/- UIl?setupbad/UIlIrelcom r/- T308?timeout/- UIl?setupbad/UIlIrelcom r/- UIl?setup/UIl!setupack UIlTsetupbad/- UIl?info/UIlI info r/- UIl?setup/UIl!setupack UIlTsetup/- UIl?info/UIlIinfo r/- UIlTsetup/UIlIsetupack UIl?rel/UIlIrelcom UIl?setupbad/UIlIrelcom r/- UIlTsetup/UIlIsetupack T302?timeout/UIlIprog.UIlI disc T305?timeout/UIlIrel r/- UIlTsetup/UIlIsetupack NI2?netclear/- UIl?info/UIlI info r/- UIlTsetup/UIlIsetupack NI2?netalert/- UIl?info/UIlI info r/- UIlTsetup/UIlIsetupack NI2?netconn/- UIl?info/UIlI info r/- UIlTsetup/UIlIsetupack UIlTconnack/- UIlTinfo/UIlI info r/- UIlTsetup/UIlIsetupack T305Ttimeout/- UIlTinfo/UIlI info r/- UIlTsetup/UIlIsetupack T308Ttimeout/- UIlTinfo/UIlIinfo r/- UIlTsetup/UIlIsetupack UIlTinfo/UIlIinfo UIlTsetupbad/- UIlTinfo/null r/- UIlTsetup/UIlIsetupack UIlTinfo/UIlIinfo UIlTsetup/- UIlTinfo/null r/- UIlTsetup/UIlIsetupack UIlTinfo/UIlIinfo UIlTinfo/null UIlTinfo/null r/- UIlTsetup/UIlIsetupack UIlTinfo/UIlIinfo UIlTinfobad/UIlIprog.UIlI disc 172 T305?timeout/UIl!rel r/- UIl?setup/UIl!setupack UIl?info/UIl!info UIl?infolast/UIl!disc NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?info/UIl!info UIl?rel/UIlirelcom UIl?setupbad/UIlirelcom r/- UIl?setup/UIl!setupack UIl?info/UIl!info UIl?disc/UIl!rel UIl?disc/null r/- UIl?setup/UIl!setupack UIl?info/UIl!info T302?timeout/UIliprog.UIl!disc T305?timeout/UIl!rel r/- UIl?setup/UIl!setupack UIl?info/UIl!info NI2?netclear/- UIl?info/null r/- UIl?setup/UIl!setupack UIl?info/UIl!info NI2?netalert/- UIl?info/null r/- UIl?setup/UIl!setupack UIl?info/UIl!info NI2?netconn/- UIl?info/null r/- UIl?setup/UIl!setupack UIl?info/UIl!info UIl?connack/- UIl?info/null r/- UIl?setup/UIl!setupack UIl?info/UIl!info T305?timeout/- UIl?info/null r/- UIl?setup/UIl!setupack UIl?info/UIl!info T308?timeout/- UIl?info/null r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc UIl?setupbad/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc UIl?setup/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UI1!callproc UIl?info/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UI1!callproc UIl?infobad/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UI1!callproc UIl?infolast/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc UIl?rel/UIlIrelcom UIl?setupbad/UIlIrelcom r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc UIl?disc/UIl!rel UIl?disc/null r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UI1!callproc T302?timeout/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc NI2?netclear/UIl!disc T305?timeout/UIl!rel r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc NI2?netconn/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc UIl?connack/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc T305?timeout/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc T308?timeout/-NI2?netalert/UIl!alert r/- UIl?setup/UIl!setupack UIl?infolast/UIl!info.UIl!callproc NI2?netalert/UIl!alert UIl?setupbad/- NI2?netconn/UIl!conn 173 r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIl!info.UI1!callproc NI2?netalert/UIl!alert UIlTsetup/- NI2Tnetconn/UIl!conn r/- UIlTsetup/UIl!setupack UIlTinfolast/UIl!info.UI1!callproc NI2Tnetalert/UIl!alert UIlTinfo/- NI2Tnetconn/UIl!conn r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIl!info.UI1Icallproc NI2Tnetalert/UIl!alert UIlTinfobad/- NI2Tnetconn/UIl!conn r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIl!info.UI1!callproc NI2Tnetalert/UIl!alert UIlTinfolast/- NI2Tnetconn/UIl!conn r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlIinfo.UI1Icallproc NI2Tnetalert/UIl!alert UIlTrel/UIlIrelcom UIlTsetupbad/UIlIrelcom r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc - NI2Tnetalert/UIl!alert UIlTdisc/UIlIrel UIlTdisc/null r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI27netalert/UIl!alert T302Ttimeout/- NI2Tnetconn/UIlI conn r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI2Tnetalert/UIl!alert NI2Tnetclear/UIlI disc T305Ttimeout/UIlIrel r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI2Tnetalert/UIl!alert NI2Tnetalert/- NI2Tnetconn/UIlI conn r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI2Tnetalert/UIl!alert UIlTconnack/- NI2Tnetconn/UIlI conn r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI2Tnetalert/UIl!alert T3057timeout/- NI2Tnetconn/UIlI conn r/-UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI2Tnetalert/UIl!alert T308Ttimeout/- NI2Tnetconn/UIlI conn r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI2Tnetalert/UIl! alert NI2Tnetconn/UIlI conn UIlTsetupbad/-UIlTconnack/null r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI2Tnetalert/UIl!alert NI2Tnetconn/UIlI conn UIlTsetup/- UIlTconnack/null r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI2Tnetalert/UIl!alert NI2Tnetconn/UIlI conn UIlTinfo/- UIlTconnack/null r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlIinfo.UI1Icallproc NI2Tnetalert/UIl!alert NI2Tnetconn/UIlI conn UIlTinfobad/- UIlTconnack/null r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlI info.UI11callproc NI27netalert/UIl!alert NI2Tnetconn/UIlI conn UIlTinfolast/- UIlTconnack/null r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlIinfo.UI1Icallproc NI2Tnetalert/UIl!alert NI2Tnetconn/UIlI conn UIlTrel/UIlIrelcom UIlTsetupbad/UIlIrelcom r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlIinfo.UIlIcallproc NI2Tnetalert/UIl!alert NI2Tnetconn/UIlI conn UIlTdisc/UIlIrel UIlTdisc/null r/- UIlTsetup/UIlIsetupack UIlTinfolast/UIlIinfo.UI1Icallproc NI2Tnetalert/UIl!alert NI2Tnetconn/UIlI conn T302Ttimeout/- UIlTconnack/null 174 /- UIlTsetup/UIlIsetupack UIlTinfolast/UIlIinfo.UIlIcallproc NI2?netalert/UIl!alert NI2?netconn/UIl!conn NI2?netclear/UIl!disc T305Ttimeout/UIl!rel /- UIl?setup/UIl!setupack UIlTinfolast/UIl!info.UI1!callproc NI2?netalert/UIl!alert NI2?netconn/UIl!conn NI2?netalert/- UIl?connack/null /- UIl?setup/UIl!setupack UIlTinfolast/UIl!info.UI1!callproc NI2?netalert/UIl!alert NI2Tnetconn/UIlI conn NI2?netconn/- UIlTconnack/null /- UIl?setup/UIl!setupack UIlTinfolast/UIl!info.UI1!callproc NI2Tnetalert/UIl!alert NI2Tnetconn/UIl!conn UIlTconnack/null UIlTconnack/null /- UIlTsetup/UIlIsetupack UIlTinfolast/UIl!info.UI1!callproc NI2Tnetalert/UIl!alert NI2Tnetconn/UIl!conn T305Ttimeout/- UIlTconnack/null /- UIlTsetup/UIlisetupack UIlTinfolast/UIl!info.UI1!callproc NI2Tnetalert/UIl!alert NI2Tnetconn/UIl!conn T308Ttimeout/- UIlTconnack/null /- UIlTsetup/UIlIsetupack UIlTinfobad/UIlIprog.UIl!disc UIlTsetupbad/-T305Ttimeout/UIl!rel /- UIlTsetup/UIlisetupack UIlTinfobad/UIliprog.UIl!disc UIlTsetup/-T305Ttimeout/UIl!rel /- UIlTsetup/UIlisetupack UIlTinfobad/UIlIprog.UIl!disc UIlTinfo/-T305Ttimeout/UIl!rel /- UIlTsetup/UIlisetupack UIlTinfobad/UIliprog.UIlidisc UIlTinfobad/-T305Ttimeout/UIlirel /- UIlTsetup/UIlisetupack UIlTinfobad/UIlIprog.UIlidisc UIlTinfolast/-T305Ttimeout/UIl!rel 7 - UIlTsetup/UIlisetupack UIlTinfobad/UIliprog.UIl!disc UIlTrel/UIl!relcom UIlTsetupbad/UIlirelcom /- UIlTsetup/UIlisetupack UIlTinfobad/UIlIprog.UIlidisc UIlTdisc/UIl!rel UIlTdisc/null /- UIlTsetup/UIlisetupack UIlTinfobad/UIlIprog.UIlidisc T302Ttimeout/-T3057timeout/UIl!rel /- UIlTsetup/UIlisetupack UIlTinfobad/UIliprog.UIlidisc NI2Tnetclear/-T305Ttimeout/UIl!rel /- UIlTsetup/UIlisetupack UIlTinfobad/UIliprog.UIlIdisc NI2Tnetalert/-T305Ttimeout/UIlIrel /- UIlTsetup/UIlIsetupack UIlTinfobad/UIliprog.UIlidisc NI2Tnetconn/-T305Ttimeout/UIlirel /- UIlTsetup/UIlisetupack UIlTinfobad/UIliprog.UIlidisc UIlTconnack/-T305Ttimeout/UIl!rel /- UIlTsetup/UIlisetupack UIlTinfobad/UIliprog.UIlidisc T3057timeout/UIl!rel UIlTdisc/null /- UIlTsetup/UIlisetupack UIlTinfobad/UIliprog.UIlIdisc T308Ttimeout/-T305Ttimeout/UIlIrel 175 r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel UIl?setupbad/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel UIl?setup/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel UIl?info/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel UIl?infobad/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel UIl?infolast/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel UIl?rel/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel UIl?disc/null UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel T302?timeout/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel NI2?netclear/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel NI2?netalert/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel NI2?netconn/- UIl?disc/null r/-. UIl?setup/UIl!setupack UIl?disc/UIl!rel UIl?connack/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel T305?timeout/- UIl?disc/null r/- UIl?setup/UIl!setupack UIl?disc/UIl!rel T308?timeout/UIl!rel UIl?setupbad/UIl!relcom 176 Appendix B DS Test Sequences for T C P connection management protocol r/- CONNECT/SYN CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- T2_outISTEN/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- SEND/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CLOSE/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- SYN/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- ACK/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- SYN_ACK/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- FIN/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- FIN_ACK/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- RST/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- Tl_out/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- T2_out/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- T2_outISTEN/null CONNECT/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null 177 CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null T2_outISTEN/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SEND/SYN CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- T2_outISTEN/null CLOSE/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- T2_outISTEN/null SYN/SYN.ACK CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null ACK/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null ' CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN_ACK/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null FIN/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null FIN_ACK/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null RST/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null Tl_out/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null T2_out/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN.ACK CONNECT/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN.ACK T2_outISTEN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN_ACK SEND/null CONNECT/null SYN_ACK/null SEND/null 178 FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN_ACK CLOSE/FIN CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN_ACK SYN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN_ACK ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- T2_outISTEN/null SYN/SYN_ACK SYN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN.ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN_ACK FIN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN.ACK FIN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN_ACK RST/null CONNECT/null SYN_ACK/null SEND/SYN FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN.ACK Tl_out/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- T2_outISTEN/null SYN/SYN_ACK T2_out/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN CONNECT/null CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN T2_outISTEN/null CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SEND/null CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN CLOSE/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN/SYN_ACK CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/ACK FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null 179 r/- CONNECT/SYN ACK/null CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN.ACK/ACK CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN FIN/null CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN FIN_ACK/null CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN RST/null CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN Tl_out/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN T2_out/null CONNECT/null SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK CONNECT/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK T2_outISTEN/null CONNECT/null SYN_ACK/null . SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK SEND/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN.ACK/ACK CLOSE/FIN CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN.ACK/ACK SYN/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN.ACK/ACK ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK SYN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN_ACK/null CONNECT/null SYN_ACK/null SEND/null 180 FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK RST/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK Tl_out/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK T2_out/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN CONNECT/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN T2_outISTEN/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN SEND/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN.ACK/ACK CLOSE/FIN CLOSE/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN SYN/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN SYN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN.ACK/ACK CLOSE/FIN RST/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN Tl_out/null CONNECT/null SYN_ACK/null 181 . SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN T2_out/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK CONNECT/null CONNECT/null. SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK T2_outISTEN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK SEND/null CONNECT/null SYN^ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r / - CONNECT/SYN SYN.ACK/ACK CLOSE/FIN FIN/ACK CLOSE/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK SYN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK SYN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK FIN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null -T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK FIN_ACK/mill CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK RST/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK Tl_out/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN/ACK T2_out/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null CONNECT/null CONNECT/null 182 SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null T2_outISTEN/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null SEND/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null CLOSE/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN.ACK/ACK CLOSE/FIN ACK/null SYN/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null SYN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null FIN/ACK CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null FIN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null RST/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null Tl_out/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN ACK/null T2_out/null CONNECT/null SYN_ACK/null SEND/null FIN/ACK CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK CONNECT/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK T2_outISTEN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK SEND/null CONNECT/null 183 SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK CLOSE/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK SYN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK SYN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK FIN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK FIN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN.ACK/ACK CLOSE/FIN FIN_ACK/ACK RST/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN.ACK/ACK Tl_out/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/SYN ACK/null CONNECT/null r/- CONNECT/SYN SYN_ACK/ACK CLOSE/FIN FIN_ACK/ACK T2_out/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CONNECT/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK T2_outISTEN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK SEND/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK SYN/null CONNECT/null SYN_ACK/null 184 SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK SYN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN.ACK/ACK FIN/ACK FIN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK FIN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK RST/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN.ACK/ACK FIN/ACK Tl_out/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK T2_out/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN CONNECT/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r / ' r CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN T2_outISTEN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN SEND/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN CLOSE/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN SYN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN ACK/null CONNECT/SYN SYN_ACK/ACK SEND/null FIN/ACK CLOSE/FIN FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN.ACK/ACK FIN/ACK CLOSE/FIN SYN_ACK/null CONNECT/null 185 SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN FIN/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN FIN_ACK/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN.ACK/ACK FIN/ACK CLOSE/FIN RST/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN Tl_out/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN r/- CONNECT/SYN SYN_ACK/ACK FIN/ACK CLOSE/FIN T2_out/null CONNECT/null SYN_ACK/null SEND/null FIN/null CLOSE/null FIN_ACK/null FIN/null T2_out/null CONNECT/null ACK/null CONNECT/SYN 186 Appendix C All T-indistingushable FSMs for the sample F S M Target Machine (same for a l l test sequences): c a b SO z/2, x/0, x/3, SI x/1, x/0, y/3, S2 z/1, y/3, x/3, S3 x/1, y/0, y / i , (1) TI: Q f l T T T T T n M 1 — o U L . U l J . U r J 1 c a b SO z/2, x/0, x/3, SI x/1, x/0, y/3, S2 z/1, y/3, x/3, S3 x/1, y/0, y / i , Conforming solution! total solutions = 1, non-conforming solutions = 0 (2) T2: ===== SOLUTION 2 == c b a 50 : z/1, x/2, y/2, 51 : z/2, y/2, x/0, 187 ===== SOLUTION 1 == c b a 50 : z/1, x/2, y/2, 51 : z/2, y/2, x/0, 52 : x/1, y/2, y/3, 53 : z/0, x/2, x/3, Non-conforming solution! ===== SOLUTION 3 ===== c b a 50 : z/1, x/3, x/O, 51 : z/2, x/3, y/3, 52 : x/2, y/3, x/0, 53 : x/2, y/2, y/0, Conforming solution! ===== SOLUTION 5 ===== c b a 50 : z/1, x/3, x/0, 51 : z/2, x/3, y/3, 52 : x/2, y/3, x/O, 53 : x/3, y/3, y/O, Non-conforming solution! ===== SOLUTION 7 ===== c b a 50 : z/1, x/3, x/0, 51 : z/2, x/3, y/3, 52 : x/3, y/3, x/0, 53 : x/3, y/3, y/0, Non-conforming solution! ===== SOLUTION 9 ===== c b a 50 : z/3, x/2, x/0, 51 : z/2, y/2, x/3, 52 : x/1, y/2, y/O, 53 : z/1, x/2, y/2, Non-conforming solution! 52 : x/2, y/2, y/3, 53 : z/O, x/2, x/3, Non-conforming solution! ===== SOLUTION 4 ===== c b a 50 : z/1, x/3, x/O, 51 : z/2, x/3, y/3, 52 : x/2, y/3, x/0, 53 : x/2, y/3, y/O, Non-conforming solution! ===== SOLUTION 6 ===== c b a 50 : z/1, x/3, x/0, 51 : z/2, x/3, y/3, 52 : x/3, y/3, x/O, 53 : x/2, y/3, y/O, Non-conforming solution! ===== SOLUTION 8 ===== c b a 50 : z/3, x/2, x/0, 51 : z/2, y/2, x/3, 52 : x/1, y/1, y/O, 53 : z/1, x/2, y/2, Non-conforming solution ===== SOLUTION 10 ===== c b a 50 : z/3, x/2, x/0, 51 : z/2, y/2, x/3, 52 : x/2, y/2, y/0, 53 : z/1, x/2, y/2, Non-conforming solution total solutions = 10, non-conforming solutions = 9 (3) T3: SOLUTION 1 ===== ===== SOLUTION 2 = c b a c b a 188 50 : z/O, y/O, y/1, 51 : x/O, x/1, x/2, 52 : z/2, x/3, y/O, 53 : -/-, y / i , y / i , Non-conforming solution! ===== SOLUTION 3 ===== c b a 50 : z/O, y/2, y/3, 51 : x/O, y/O, x/3, 52 : x/O, y/1, y/1, 53 : z/3, x/2, y/2, Non-conforming solution! ===== SOLUTION 5 ===== c b a 50 : z/2, y/O, y/1, 51 : x/O, x/1, x/3, 52 : z/O, y/1, y/1, 53 : z/3, x/2, y/O, Non-conforming solution! ===== SOLUTION 7 ===== c b a SO : z/2, x/1, x/3, SI : x/1, y/2, x/3, S2 : z / i . y / i , y/o, S3 : z/3, x/2, y/2, Non-•conforming solution! SO z/O, y/O, y / i , SI x/O, x/3, x/2, S2 z/2, x/3, y/o, S3 x/O, y/1, y / i , Non-c onf orming solution — QHT TTTTflff A c b a SO z/O, y/2, y/3, SI x/O, y/O, x/3, S2 x/1, y/1, y / i , S3 z/3, x/2, y/2, Non-c onf orming solution == SOLUTION 6 ===== c b a 50 : z/2, y/1, y/2, 51 : x/1, y/O, x/3, 52 : z/1, x/1, x/3, 53 : z/3, x/O, y/O, Non-conforming solution ===== SOLUTION 8 ===== c b a 50 : z/2, x/3, x/O, 51 : x/1, y/3, x/O, 52 : z/1, x/3, y/3, 53 : x/1, y/1, y/O, Conforming solution! ===== SOLUTION 9 ===== c b a 50 : z/2, y/1, y/1, 51 : x/2, x/1, x/3, 52 : z/2, y/2, y/1, 53 : z/3, x/O, y/2, Non-conforming solution! total solutions = 9, non-conforming solutions = 8 (4) T4: 1 8 9 ===== SOLUTION 1 ===== c a b 50 : z/O, y/O, y/3, 51 : x/O, x/3, x/2, 52 : z/1, y/1, x/1, 53 : z/2, y/2, y/O, Non-conforming solution! ===== SOLUTION 3 ===== c a b 50 : z/O, y/O, y/3, 51 : x/3, x/3, x/2, 52 : z/1, y/1, x/1, 53 : z/2, y/2, y/3, Non-conforming solution! ===== SOLUTION 5 ===== c a b 50 : z/O, y/2, y/O, 51 : x/3, x/3, x/3, 52 : z/1, y/O, x/1, 53 : z/2, y/1, y/O, Non-conforming solution! ===== SOLUTION 7 ===== c a b 50 : z/1, x/2, y/1, 51 : x/O, y/3, y/1, 52 : z/O, x/3, x/3, 53 : z/2, y/2, x/1, Non-conforming solution! ===== SOLUTION 9 ===== c a b 50 : z/2, x/O, x/1, 51 : x/1, y/O, y/1, 52 : z/3, y/1, x/1, 53 : x/1, x/O, y/1, Non-conforming solution! ===== SOLUTION 11 ===== c a b ===== SOLUTION 2 ===== c a b 50 : z/O, y/O, y/3, 51 : x/O, x/3, x/2, 52 : z/1, y/1, x/1, 53 : z/2, y/2, y/3, Non-conforming solution! ===== SOLUTION 4 ===== c a b 50 : z/O, y/2, y/O, 51 : x/O, x/3, x/3, 52 : z/1, y/O, x/1, 53 : z/2, y/1, */*, Non-conforming solution! ===== SOLUTION 6 ===== c a b 50 : z/O, y/3, y/O, 51 : x/O, x/3, x/2, 52 : z/1, y/1, x/2, 53 : z/2, y/O, x/1, Non-conforming solution! ===== SOLUTION 8 ===== c a b 50 : z/1, x/2, */*, 51 : x/1, y/3, y/1, 52 : z/O, x/3, x/3, 53 : z/2, y/2, x/1, Non-conforming solution ===== SOLUTION 10 ===== c a b 50 : z/2, x/O, x/1, 51 : x/1, y/O, y/1, 52 : z/3, y/1, x/1, 53 : x/3, x/O, y/1, Non-conforming solution ===== SOLUTION 12 ===== c a b 190 50 : z/2, x/O, x/1, 51 : x/1, y/O, y/1, 52 : z/3, y/1, x/1, 53 : z/1, x/2, y/1, Non-conforming solution! ===== SOLUTION 13 ===== c a b 50 : z/2, x/O, x/1, 51 : x/3, y/O, y/1, 52 : z/3, y/1, x/1, 53 : x/3, x/O, y/1, Non-conforming solution! ===== SOLUTION 15 ===== c a b 50 : z/2, x/O, x/1, 51 : x/3, y/0, y/3, 52 : z/3, y/1, x/1, 53 : x/3, x/0, y/1, Conforming solution! ===== SOLUTION 17 ===== c a b 50 : z/2, x/0, x/1, 51 : x/1, y/0, y/1, 52 : z/3, y/2, x/1, 53 : z/1, x/2, */*, Non-conforming solution! ===== SOLUTION 19 ===== c a b 50 : z/2, x/0, x/1, 51 : x/3, y/0, y/1, 52 : z/3, y/2, x/1, 53 : z/1, x/2, y/1, Non-conforming solution! ===== SOLUTION 21 ===== c a b 50 : z/2, x/O, x/3, 51 : x/1, x/0, y/2, 50 : z/2, x/0, x/1, 51 : x/3, y/0, y/1, 52 : z/3, y/1, x/1, 53 : x/1, x/0, y/1, Non-conforming solution! ===== SOLUTION 14 ===== c a b 50 : z/2, x/O, x/1, 51 : x/3, y/0, y/1, 52 : z/3, y/1, x/1, 53 : z/1, x/2, y/1, Non-conforming solution! ===== SOLUTION 16 ===== c a b 50 : z/2, x/O, x/1, 51 : x/3, y/O, y/3, 52 : z/3, y/1, x/1, 53 : z/1, x/2, y/1, Non-conforming solution! ===== SOLUTION 18 ===== c a b 50 : z/2, x/O, x/1, 51 : x/2, y/0, y/1, 52 : z/3, y/2, y/2, 53 : z/1, x/2, x/1, Non-conforming solution ===== SOLUTION 20 ===== c a b 50 : z/2, x/0, x/3, 51 : x/1, x/0, y/2, 52 : z/1, y/3, y/1, 53 : z/0, y/0, x/1, Non-conforming solution ===== SOLUTION 22 ===== c a b 50 : z/2, x/0, x/3, 51 : x/2, x/0, y/2, 191 52 : z/1, y/3, y/2, 53 : z/O, y/O, x/1, Non-conforming solution! 52 : z/1, y/3, y/2, 53 : z/O, y/O, x/1, Non-conforming solution ===== SOLUTION 23 ===== ===== SOLUTION 24 ===== c a b c a b SO : z/2, y/1, x/O, SO : z/3, x/2, x/1, SI : x/2, x/O, x/O, SI : x/1, y/O, y/ i , S2 : z/1, y/3, y/2, S2 : z/2, x/O, */*, S3 : z/O, y/3, x/1, S3 : z/1, y/1, x/1, Non-c onf orming solution! Non-conforming solution ===== SOLUTION 25 ===== c a b 50 : z/3, x/2, x/1, 51 : x/2, y/O, y/1, 52 : z/2, x/O, y/1, 53 : z/1, y/1, x/1, Non-conforming solution! == SOLUTION 27 ===== c a b SO : z/3, y/1, x/1, SI : x/3, x/3, x/O, S2 : z/1, y/O, y/2, S3 : z/2, y/2, y/3, Non-•conforming solution! ===== SOLUTION 26 ===== c a b 50 : z/3, y/1, x/1, 51 : x/2, x/3, x/O, 52 : z/1, y/O, y/2, 53 : z/2, y/2, x/O, Non-conforming solution total solutions = 27, non-conforming solutions = 26 (5) T2a: ===== SOLUTION 1 ===== c b a 50 : z/2, x/1, x/O, 51 : x/1, y/1, y/O, 52 : z/3, x/1, y/1, 53 : x/1, y/1, x/O, Non-conforming solution! ===== SOLUTION 2 ===== c b a 50 : z/2, x/1, x/O, 51 : x/1, y/1, y/O, 52 : z/3, x/1, y/1, 53 : x/3, y/1, x/O, Non-conforming solution SOLUTION 3 ===== ===== SOLUTION 4 = c b a c b a 192 50 : z/2, x/1, x/O, 51 : x/3, y/1, y/O, 52 : z/3, x/1, y/1, 53 : x/1, y/1, x/O, Non-conforming solution! ===== SOLUTION 5 ===== c b a 50 : z/2, x/1, x/0, 51 : x/3, y/3, y/O, 52 : z/3, x/1, y/1, 53 : x/3, y/1, x/O, Conforming solution! 50 : z/2, x/lf x/0, 51 : x/3, y/1, y/0, 52 : z/3, x/1, y/1, 53 : x/3, y/1, x/0, Non-conforming solution total solutions = 5, non-conforming solutions = 4 193 

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

Usage Statistics

Share

Embed

Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                        
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            src="{[{embed.src}]}"
                            data-item="{[{embed.item}]}"
                            data-collection="{[{embed.collection}]}"
                            data-metadata="{[{embed.showMetadata}]}"
                            data-width="{[{embed.width}]}"
                            async >
                            </script>
                            </div>
                        
                    
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:
https://iiif.library.ubc.ca/presentation/dsp.831.1-0051312/manifest

Comment

Related Items