Network Protocol System Passive Testing for Fault Management - a Backward Checking Approach - PDF

Please download to get full document.

View again

of 17
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information Report
Category:

Ancient Egypt

Published:

Views: 2 | Pages: 17

Extension: PDF | Download: 0

Share
Related documents
Description
Network Protocol System Passive Testing for Fault Management - a Backward Checking Approach Baptiste Alcalde 1, Ana Cavalli 1, Dongluo Chen 2, Davy Khuu 1, and David Lee 3 1 Institut National des Télécommunications
Transcript
Network Protocol System Passive Testing for Fault Management - a Backward Checking Approach Baptiste Alcalde 1, Ana Cavalli 1, Dongluo Chen 2, Davy Khuu 1, and David Lee 3 1 Institut National des Télécommunications GET-INT, Evry, France {baptiste.alcalde, ana.cavalli, 2 Department of Computer Science, Tsinghua University, Beijing, China 3 Bell Labs Research, Lucent Technologies Abstract. Passive testing has proved to be a powerful technique for protocol system fault detection by observing its input/output behaviors yet without interrupting its normal operations. To improve the fault detection capabilities we propose a backward checking method that analyzes in a backward fashion the input/output trace from passive testing and its past. It effectively checks both the control and data portion of a protocol system, compliments the forward checking approaches, and detects more errors. We present our algorithm, study its termination and complexity, and report experiment results on the protocol SCP. 1 Introduction Passive testing is an activity of detecting faults in a system under test by observing its input/output behaviors without interfering its normal operations. The usual approach of passive testing consists in recording the trace produced by the implementation under test and trying to find a fault by comparing this trace with the specification ([4], [6], [7]). Other approaches explore relevant properties required for a correct implementation, and then check on the implementation traces of the systems under test ([1], [2]). Most of the work on passive testing are based on finite state machines (FSMs) and they are focused on the control part of the tested systems without taking into account data parts. To cope with protocol data portions, Extended Finite State Machines (EFSMs) are used to model the systems, which include parameters and variables to encode data. In [7] a first approach to perform passive testing on EFSMs was proposed. An algorithm based on constraints on variables was developed and applied to GSM- MAP protocol. However, this algorithm cannot detect transfer errors. In [5], an algorithm based on variable determination with the constraints on variables was presented. This algorithm allows to trace the variables values as well as the system state, however, every transfer errors still cannot be detected. To overcome this limitation, we propose a new approach based on backward tracing. This algorithm is strongly inspired by this presented in [5], but processes the trace backward in order to further narrow down the possible configurations for the beginning of the trace and to continue the exploration in the past of the trace with the help of the specification. This algorithm contains two phases. It first follows a given trace backward, from the current configuration to a set of starting ones, according to the specification. The goal is to find the possible starting configurations of the trace, which leads to the current configuration. Then it analyses the past of this set of starting configurations, also in a backward manner, seeking for end configurations, that is to say configurations in which the variables are determined. When such configurations are reached, we can take a decision on the validity of the studied path. This new algorithm is applied to Simple Connection Protocol (SCP) that allows to connect two entities after a negotiation of the quality of service required for the connection. Even it is a simple protocol it presents a number of key characteristics of real communication protocols. The testing results are compared to the passive testing algorithm in [5]. The rest of the paper is organized as follows. Section 2 describes the basic concepts used in the paper. Section 3 contains preliminary algorithms for processing transition back tracing. The section 4 presents the main backward tracing algorithm. In section 5 the issues related to the termination and complexity of the main algorithms are discussed. Section 6 reports the experiments of the algorithm on the Simple Connection Protocol. 2 Preliminaries We first introduce basic concepts needed and then present an overview of our algorithm. 2.1 Extended Finite State Machine We use Extended Finite State Machine (EFSM) to model the protocol systems. Definition 1. An Extended Finite State Machine M is a 6-tuple M = S, s 0, I, O, x, T where S is a finite set of states, s 0 is the initial state, I is a finite set of input symbols (eventually with parameters), O is a finite set of output symbols (eventually with parameters), x is a vector denoting a finite set of variables, and T is a finite set of transitions. A transition t is a 6-tuple t = s i, s f, i, o, P, A where s i and s f are the initial and final state of the transition, i and o are the input and the output, P is the predicate (a boolean expression), and A is the ordered set (sequence) of actions. Definition 2. An events trace is a sequence of I/O pairs. In this paper we consider that the traces can start at any moment of the implementation execution. Given a trace from the implementation under test and a specification, the algorithm will detect the three types of error that can occur in an EFSM. Definition 3. The three types of error are: 1. the output errors : when the output of a transition in the implementation differs from the output of the corresponding transition in the specification. 2. the transfer errors : when the ending state of a transition in the implementation differs from the ending state of the corresponding transition in the specification. 3. the mixed errors : a mix between the two errors defined above. SPECIFICATION i1/o1 or i2/o2 (2) i2/o2 (1) i1/o4 2 3 IMPLEMENTATION i2/o5 (3) Fig. 1. Output(1), transfer(2), and mixed(3) errors 2.2 Candidate Configuration Set The backward checking algorithm processes in two phases as shown in figure 2. The first step consists in following the trace w backward, from the end to the beginning, according to the specification. The goal is to arrive to the set X of possible start configurations of w. In order to keep information we use configurations named Candidate Configuration Set (CCS) inspired from [5]. past of the trace FAIL FAIL ΟΚ FAIL FAIL X back tracing of the past, in order to confirm X trace back tracing of the trace Fig. 2. Overview of Backward Checking Definition 4. Let M be an EFSM. A Candidate Configuration Set (CCS), is a 3-tuple (e, R, Assert) where e is a state of M, R is an environment (that is to say that each variable v has a constraint R(v)), and Assert is an assertion (Boolean expression). The second step is the backward checking of the trace past. This step consists in confirming at least one of the departure configurations extracted from the back tracing of a trace. It means we must verify that the variable values or constraints are compliant with the specification. We need to trace the transitions from their end states to their start states until we reach a validation criteria. We need to confirm the variables ranges. However, often there is only a subset of variables that we can confirm, and we call these variables determinant of a trace. Definition 5. A variable v is a determinant of a trace t if v must be necessarily validated before validating t. In order to keep information about determinants, we define a new structure for the past of the trace: the Extended Candidate Configuration Set (also called Extended Configuration). Definition 6. Let M be an EFSM. An Extended Candidate Configuration Set (ECCS) is a 4-tuple (e, R, Assert, D), where e is a state of M, R is an environment, Assert is an assertion, and D is a set of determinant variables. Between the two steps we check the determinant variable set as follows : every variable whose interval in a configuration of X - the set of possible start configurations of the trace that is included in its specified domain - must be added to the determinant variables set to be checked. 3 Preliminary Algorithms In the following section, we present the preliminary algorithms that will be used in the main algorithm. We begin with the inverse actions algorithm, and then consistency checking and the transition back tracing algorithms. What we do is checking backward the trace and then exploring its past as shown in Fig 2, determining the variables. In order to perform this checking on the whole trace and its past we need a process that checks a transition backward. The algorithms presented in this section make it possible. 3.1 The Inversed Actions A main difficulty is the application of the inverse action A 1. The inverse actions will be processed in a reversed order. Hence the following normal ordered actions {a 1,..., a n } will be processed in an order: {a n,..., a 1 }. Each inverse action depends on the type of the corresponding normal action. There are three types of actions: 1. w constant 2. w f(u, v,...) where w is not a variable of f 3. w f(w, u, v,...) where w is also a variable of f These three types of actions are assignations : they overwrite the value of the left variable w with the value of the right component. We note that the value of w is modified by an action, but the other variables after action keep the value they had before the action and that only the value of the variable w will be modified by back tracing a transition. Except for this, every type of action must be inverted: 1. Action of type 1. The value of w after the action is a constant. This gives us a first occasion of detecting an error. If the constant does not conform the current constraint then we are on an invalid path. Otherwise, we replace every occurrence of w with the constant and refine the constraints of other variables. However, it is impossible to know the value of w before the action; indeed, actions simply overwrite the former value of w. After the action back tracing the value of w is UNDEFINED; 2. Action of type 2. We could take that R(w) is equal to R(f(u, v,...)) but we can be more precise: it is R(w) R(f(u, v,...)). In order to keep as much information as possible, every occurrence of w will be replaced by f(u, v,...). However, the value of w before action remains UNDEFINED; 3. Action type 3. This action brings no new constraint refinement on the variable w (on the left side of the assignment) after the action (left member) but it gives a constraint on the variable w (on the right side of the assignment) before the action. Consequently, every occurrence of w will be replaced by f 1 (w). 3.2 Final Checking Phase The check consistency process is from [5] and is able to detect inconsistency in the definition of the variables by refining the intervals of variables and its constraints. There are no big differences between the transition back tracing algorithms for the trace and for its past, and we ignore in the trace algorithm what can happen to the set of determinants before the action. Indeed, in the trace we do not determine variables; we can only refine their values, and we invalid the trace if the constraints are not consistent. For the trace we must check the output before processing the inverse actions. After processing every action we can determine the variables involved in the input if its constraint is consistent with what we found. Otherwise, we invalid the transition. On the other hand, we must check that the variable values that we found are consistent with the predicates. Otherwise, the path is invalid. Therefore, in the checking we must determine if a transition is valid or not. We need a process called check pred for the past of the trace to modify the set of determinants. In the case of back tracing, we just need to add the predicates to the set of assertions and process check consistency - no specific operations are needed. The pseudo code for back tracing of the trace and of its past, followed by the check pred and check consistency algorithms are presented in the appendix. 3.3 Example We show now an example of this process. Consider the common steps of the trace and past cases, a transition without input/output, and we include the variable set D into parentheses. Starting point i P : u =1 A : x=1 y=y+1 z=v+w R = u [0;3], x [1;4], y [2;8], z [1;2], a [7;9], f v undef, w undef Asrt = - (D = {u,x,y,z,a}) After inversed actions R = u [0;3], a [7;9], y [1;7], cste [1;2], v,w undef, x,z undef Asrt = {v+w=cste} (D = {u,a,y,v,w}) After check_pred R = a [7;9], y [1;7], u [1;3], cste[1;2], v,w undef, x,z undef Asrt = {v+w=cste} (D = {u,a,y,v,w}) i i P : u =1 A : x=1 y=y+1 z=v+w R = u [0;3], x [1;1], y [2;8], z [1;2], a [7;9], f v,w undef Asrt = - (D = {u,x,y,z,a}) P : u =1 A : x=1 y=y+1 z=v+w R = u [0;3], x [1;1], y [2;8], z [1;2], a [7;9], f v,w undef Asrt = - (D = {u,x,y,z,a}) 4 Main Algorithms We are ready to present our main algorithm of backward checking. 4.1 Backward Checking of a Trace The backward checking for a whole trace can be derived from the algorithm for back tracing a transition (Back trace transition): - trace: The observed trace. gettail(trace) removes and returns the last i/o pair from trace. - X: Set of starting extended configurations from back trace of an event trace. Each configuration is a 4-tuple (e, R, Assert, D) - X : Current set of extended configurations - V : Set of known extended configurations - c : A new configuration - : Returns TRUE if the sequence is correct, and FALSE otherwise 1. V X 2. while X & i/o := gettail(trace) do 3..X 4..for each configuration c X do 5...for each transition t where t.end state = c.state and t.i/o = i/o do 6....c Back trace transition(t, c) 7....X X {c } 8....V V X 9..X X 10. return FALSE 4.2 Backward Checking of the Past of an Event Trace The backward checking algorithm applied to the past of a trace consists of a breadth-first search in the past of the configurations, which are extracted from the back tracing of a trace due to the fact that one cannot use a variable value before it is assigned. In order to validate a trace, we only need to find a path binding a set of assignments or predicates to one of the configurations extracted from back tracing. We now proceed to the main algorithm. We first define the operations and \ on the Extended Candidate Configuration Sets (ECCS) that will be used for pruning the exploration tree of the past. Then we study the path convergence and discuss the algorithm termination, the correctness and the complexity. The Operation. It is an intersection between two configurations: Definition 7. Let be three configurations c 1 = (e, R 1, Assert 1, D), c 2 = (e, R 2, Assert 2, D), and c = (e, R, Assert, D). We define the intersection operator as follows. If c = c 1 c 2, then : 1. for each variable v, R(v) = R 1 (v) R 2 (v) where is the intervals intersection operator 2. Assert = Assert 1 Assert 2 where is the boolean and operator Remark on. The configuration states and the variable sets, which are not validated yet, are the same. If they are not, the intersection equals to NULL. The \ Operation. It is a privation. Given two configurations c 1 and c 2, the result of c 1 \c 2 is a couple (c a, c b ). We obtain c a by removing c 2 from c 1, but only in case of each variable is restricted to the intersection of the intervals c 1 and c 2, respectively. c b is the rest of c 1. Definition 8. Given four configurations c 1 = (e, R 1, Assert 1, D), c 2 = (e, R 2, Assert 2, D), c a = (e, R a, Assert a, D) and c b = (e, R b, Assert b, D), we define the privation operator \ as follows. If (c a, c b ) = c 1 \c 2, then : 1. for c a : (a) for each variable v, we have got : R a (v) = R 1 (v) R 2 (v) where is the intervals intersection operator (b) Assert a = Assert 1 Assert 2, where is the boolean and operator 2. for c b : (a) R b = R 1 V 1 (b) Assert b = Assert 1 ( (v i R 2 (v i ))) where is the boolean and i=0 operator, and is the boolean or operator ( be careful of priorities of parenthesis) Remark on \. If Assert 2 equals to, then c a equals to NULL. Indeed Assert 2 means we have to keep all of the values that R 2 allows, yet on the contrary Assert 2 implies that we must delete all of them. General remark. The operations and \ may return configurations, which are inconsistent. For example, the result of c 1 \c 1 is not consistent. Moreover, some results may need to be refined. Indeed when two assertions are concatenated the constraints intervals of each variable may have to be changed. So we should use the Check consistency procedure that has already been presented. For now, we consider that the results of and \ are automatically checked and transformed by Check consistency. Examples. Consider the configurations c 1 = (e, x = [0; 5], y = [0; 3] ,, {x}) (where means no assertion) and c 2 = (e, x = [0; 2], y = [ 1; 1] , {x y}, {x}), and three configurations c i, c a and c b, which are defined as following : c i = c 1 c 2 (c a, c b ) = c 1 \c 2 We first determinate c i. R i is defined as the intersection of R 1 and R 2, and Assert i is Assert 1 Assert 2. Then we have: c i = (e, x = [0; 2], y = [0; 1], {x y}, {x}). Determinating c a and c b is a little bit more complicated. R a is the intersection of R 1 and R 2, and Assert a is Assert 1 Assert 2. Then we have : c a = (e, x = [0; 2], y = [0; 1] , {x y}, {x}). At last for c b, we have the following properties. R b equals R 1, and we must add x 0 x 2 and y 0 y 1 to Assert b. Then we have : c b = (e, x = [0; 5], y = [0; 3] , {(x 0 x 2) (y 0 y 1)}, {x}). Note that the two last configurations c a and c b are not refined as it was defined in [5]. If we apply the Check consistency procedure, we obtain : c a = (e, x = [0; 1], y = [0; 1] , {x y}, {x}) and c b = (e, x = [3; 5], y = [2; 3] ,, {x}). Path Convergence. Consider a step r of our algorithm. If we find a configuration c that we have already found earlier, in a previous step or earlier in the step r, we have got a path convergence phenomena. Definition 9. Two paths P 1 and P 2 are convergent (in the past!) if they lead to the same configuration c. Consequently both P 1 and P 2 have the same past. So we will obtain the same information if we explore the common past from P 1 or from P 2. Consider that we have first followed P 1. When we find that P 2 converges toward c, we do not continue the exploration: we prune P 2 at c. The pruning enables us to deal with the infinite exploration paths. Unfortunately extended configurations make convergences hard to be detected; they are non-empty intersections of configurations. We proceed as follows. Given three configurations c, c 1 and c 2, let c be equal to c 1 c 2. Suppose that c 2 has been found before c 1. Then we have the following: c =NULL. c 1 and c 2 are independent and the respective pasts of c 1 and c 2 must be explored; (c NULL) (c = c 1 ). c 1 is included in c 2 and we must delete c 1 ; (c NULL) (c c 1 ). c 2 is included in c 1 and we must substitute c 1 by c 1 \c 2 The algorithm Check redundancy, that will be described later, deals with the convergence cases. path P1 1 2 common past path P2 3 4 c convergence point Fig. 3. Example of Path Convergence Algorithm of Backward Checking of the Past of a Trace. The Backward checking past algorithm backward traces the past of a trace in order to validate it. The input is the set of starting extended configurations, which we extracted from the trace back tracing. Note that if the start configuration is invalid (not reachable from the initial configuration set) then we have to explore backward all the configurations to tell whether there is no valid path from the initial configuration set. However, if it is indeed valid, finding a valid path is enough. In most cases of passive testing, the traces do not contain faults and it is desirable to use a heuristic method to find a valid path. We now present such a procedure. In order to guide the heuristic search, we have figure out the end configurations. A configuration set c is an end configuration
Recommended
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks