UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

An Estelle.Z parser for a protocol test generation environment TESTGEN+ Zhang, Rui 1996

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

Item Metadata

Download

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

Full Text

A N ESTELLE.Z PARSER FOR A PROTOCOL TEST GENERATION ENVIRONMENT  TESTGEN+  By R u i Zhang B . Eng. (Computer Science) X i ' a n Jiaotong University  A THESIS SUBMITTED IN PARTIAL F U L F I L L M E N T OF T H E REQUIREMENTS FOR T H E D E G R E E OF M A S T E R OF  SCIENCE  in T H E F A C U L T Y OF G R A D U A T E STUDIES COMPUTER  SCIENCE  We accept this thesis as conforming to the required standard  T H E UNIVERSITY OF BRITISH COLUMBIA  August 1996 © R u i Zhang, 1996  In presenting this thesis i n partial fulfillment of the requirements for an advanced degree at the University of B r i t i s h C o l u m b i a , 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 m y 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 m y written permission.  Computer Science T h e University of B r i t i s h C o l u m b i a 2366 M a i n M a l l Vancouver, Canada V 6 T 1Z4  Date:  Abstract  Protocol testing is an indispensable constituent i n protocol development. T h e test suite generation and selection processes are usually tedious and time-consuming. is difficult to manually generate and select test suites without errors.  It  Therefore, an  automatic protocol test suite generation and selection environment is required. For this purpose, the protocol test suite generation and selection environment, T E S T G E N + , was developed. T E S T G E N + includes the T E S T G E N , T E S T S E L and T E S T V A L tools for test suite generation, selection, and validation, respectively. In this thesis, a new front end of the T E S T G E N tool, an Estelle.Z parser which is for an Estelle-like protocol specification language, is designed and implemented. A real world protocol, home agent - a major component of the M o b i l e I P protocol, is specified in Estelle.Z. T h e specification is fed into the T E S T G E N tool to yield a test suite, which is then fed into the T E S T S E L tool to get a subset of an efficient test suite w i t h user satisfactory coverage and cost. In order to evaluate the correctness of the parser, the same protocol is specified i n E s t e l l e . Y + A S N . l and fed through a different parser into T E S T G E N and T E S T S E L generating a test suite. C o m p a r i n g the two test suites, results from the experiment indicate: a) the Estelle.Z parser works w i t h the T E S T G E N tool well; b) T E S T G E N and T E S T S E L are competent tools to generate and select test suites for protocol specifications; c) furthermore, there is room to improve the T E S T G E N and the T E S T S E L tools.  11  Table of Contents  Abstract  ii  List of Tables  vi  List of Figures  vii  Acknowledgment 1  2  3  ix  Introduction  1  1.1  Thesis M o t i v a t i o n and Contributions  1.2  Thesis Outline  *  1 "  2  T E S T G E N + Environment  4  2.1  Test Suite Generation - T E S T G E N  6  2.2  Test Suite Selection - T E S T S E L  8  2.3  Test Suite Validation - T E S T V A L  11  Estelle.Z Parser for T E S T G E N  13  3.1  Introduction  13  3.2  Estelle.Z Language  14  3.3  Implementation of Estelle.Z Parser  18  3.3.1  Lexical Analysis of Estelle.Z  18  3.3.2  Syntax Analysis of Estelle.Z  18  in  4  3.3.3  Semantic Analysis  22  3.3.4  Structure of the P D S  23  3.3.5  Testing for the parser  28  3.4  Improvement on the interface of T E S T G E N  29  3.5  Summary  32  Specification of a Subset of the M o b i l e IP P r o t o c o l  33  4.1  Basics of the Protocol  34  4.1.1  Protocol Overview  35  4.1.2  Home Agent  36  4.1.3  Foreign Agent  37  4.1.4  Mobile Host  38  4.1.5  5  Example  39  4.2  Home Agent  42  4.3  T h e formal Specifications of the Home Agent  45  A p p l y i n g M o b i l e IP to T E S T G E N 5.1  The Test Suite Generation 5.1.1  5.2  5.3  51 •  The A l g o r i t h m of T E S T G E N  51 '  52  5.1.2  Constraints of T E S T G E N  54  5.1.3  Comments on T E S T G E N  57  The Coverage O f The Test Suite  60  5.2.1  T h e algorithm of the test selection tool  60  5.2.2  The results of the T E S T S E L  62  Results from the Estelle.Z parser  66  iv  5.4 6  Summary  67  Conclusions and Future W o r k  70  6.1  Conclusions  70  6.2  Future Work  71  Bibliography  74  Appendices  75  A  A S N . l specification of the simplified H o m e Agent in M o b i l e IP  75  B  E s t e l l e . Y specification of the simplified H o m e Agent in M o b i l e IP  80  C  Estelle.Z specification of the simplified H o m e Agent in M o b i l e IP  96  D  ASN.l  specification  of message parameters for the  complete H o m e  Agent  115  E  Selected C o n t r o l Sequences and Test Cases  125  F  4 T y p i c a l Control Sequences and T y p i c a l test cases in T T C N . M P  137  List of Tables  4.1  Fields i n Registration Request  42  4.2  Fields i n Registration Reply  43  4.3  Fields i n Advertisement  44  5.1  Results of the T E S T S E L for Specification i n E s t e l l e . Y + A S N . l  63  5.2  Results of the T E S T S E L for Specification i n Estelle.Z  69  vi  List of Figures  2.1  TESTGEN+Environment  .  5  2.2  T E S T G E N Structure  2.3  T E S T S E L Structure  2.4  T E S T V A L Structure  3.1  E x a m p l e of the Declaration Component  3.2  E x a m p l e of the Initialization Component  17  3.3  E x a m p l e of the Transition Component  17  3.4  Estelle.Z Parser Generation  19  3.5  Syntax Tree of Assignment Statement  20  3.6  Structure of Constant Declaration  20  3.7  Syntax Tree of Channel Declaration ( P D U )  21  3.8  Syntax Tree of State Transition  23  3.9  Environment of the Parser  24  7 '  9 11 ,  15  3.10 Protocol D a t a Structure  25  3.11 D a t a Structure of State i n the P D S  26  3.12 Architecture of T T C N Tree F r o m T E S T G E N  "  31  4.1  M o d u l e of M o b i l e IP  34  4.2  E x a m p l e of mobile IP Operation  40  4.3  E F S M of the Home Agent  48  vii  5.1  Test Case Space  61  5.2  T w o Parsers  68  vm  Acknowledgment  First of all, I would like to express m y sincerest appreciation to m y supervisor, D r . Son Vuong, for his constant encouragement and invaluable guidance throughout m y research work, which made it possible for me to complete this thesis on time. His enthusiasm has made the past years an enjoyable and unforgettable period. I would like to thank D r . N o r m Hutchinson for his helpful comments and careful reading of the final draft despite his very busy schedule. I wish to thank D r . ir. R o l f J . Velthuys and M r . B i n h D o for their helpful suggestions and productive discussions, and M s . A n d r e a Warrington who read the thesis draft and made very good suggestions to improve the thesis. I wish to acknowledge the Computer Science department at the University of B r i t i s h C o l u m b i a for providing an environment suitable for m y research and for providing financial support. T h e financial support i n the form of R A from the joint grant of M o t o r o l a and N S E R C / I O R is also gratefully acknowledged. I wish to thank m y relatives and friends who gave me constant encouragement and moral support during m y studies i n Canada. I wish to express my gratitude and appreciation to m y husband Y i d o n g and m y daughter Jenny for their unceasing support and understanding. W i t h o u t their patience and support, this thesis could not have been completed.  IX  Chapter 1  Introduction  1.1  Thesis M o t i v a t i o n and Contributions In general, a communication protocol is quite complex and takes a considerable effort  to move from a standard protocol specification to an implementation on a real system. T h e protocol standard may lead to several different implementations.  T h e testing of  each protocol implementation for conformance to the specification of the protocol standard becomes critical.  T h e complexity of protocols necessitates the use of automated  tools to test the protocol implementation. For this purpose, the T E S T G E N - | - environment was developed to generate test suites based on the protocol specifications i n the E s t e l l e . Y + A S N . l language.  In T E S T G E N + , there are three major modules:  TEST-  G E N , T E S T S E L and T E S T V A L for test suite generation, test suite selection and test suite verification respectively. T E S T G E N + accepts E s t e l l e . Y + A S N . l specifications and yields test suites. T h e Estelle language is one of the F D T s (Formal Description Techniques) based on an extended state transition model. A subset of Estelle defined as Estelle.Z is employed i n T E S T G E N + , because the complete Estelle language is too complex and the T E S T G E N kernel does not support it. In this thesis, the research objectives are: • To design and develop the front end of the testing environment T E S T G E N + for  1  Chapter 1.  Introduction  2  Estelle.Z. • To demonstrate the usefulness of the tools, T E S T G E N and T E S T S E L , by applying it to a real world protocol and generating a test suite for the protocol. • To prove the parser works correctly by applying the real world protocol specification to it. T h e front end of the testing environment is the essential constituent of the whole test environment. It analyzes the protocol specification, which is the m a i n information given by the user. In addition, it provides the internal representation of the protocol i n which the external behaviors of a protocol are precisely and completely described. T h e internal representation of protocol must be accessible to the T E S T G E N engine, which is the key process of the whole testing generation environment. T h e M o b i l e I P protocol is a well-known real world protocol.  In this thesis, it is  employed to test the new parser and the T E S T G E N + tool. T h e home agent, a major component of M o b i l e IP, is specified i n both Estelle.Z and E s t e l l e . Y + A S N . l languages. These specifications are fed into the T E S T G E N + tool to yield two sets of test suites. Results from the experiment indicate that the parser works w i t h the T E S T G E N engine. They also indicate that while the T E S T G E N + environment is an efficient tool, it can still be improved further.  1.2  Thesis Outline T h e rest of this thesis is organized as follows. In chapter 2, an overview of the T E S T -  G E N + environment is introduced. A n introduction to each m a i n module i n T E S T G E N + and the architecture of T E S T G E N + are presented.  Chapter  1.  Introduction  3  In chapter 3, the design and implementation of the front end of T E S T G E N are discussed. T h e definition and function of the Estelle.Z language are introduced, the object data structure of the internal representation of protocol is described, and then the i m plementation of the Estelle.Z parser is presented. In chapter 4, a review of a real world protocol, home agent - a component of M o b i l e IP, is given first. T h e protocol is specified i n Estelle.Y for the control component and specified i n A S N . l for the data component. Also the protocol specification i n Estelle.Z is presented. In chapter 5, T h e applications of T E S T G E N + to both the specifications given i n chapter 4 are discussed, and the results are analyzed. A t the end, the strong points and weak points of T E S T G E N and T E S T S E L are discussed. In chapter 6, Some conclusions are drawn and future improvement work on the parser, T E S T G E N and T E S T S E L is discussed. T h e appendices contain listings of files used i n the thesis. T h e source codes for the specification i n A S N . l and Estelle.Y are shown i n A p p e n d i x A and B respectively. T h e source code for the specification i n Estelle.Z is shown i n A p p e n d i x C . T h e complete home agent message parameters specification i n A S N . l is shown i n A p p e n d i x D . T h e selected control sequences and the subset of selected test cases are shown i n A p p e n d i x E . T h e test cases i n T T C N (Tree and Tabular Combined Notation) form are shown i n A p p e n d i x  Chapter 2  TESTGEN+  Environment  Introduction Protocol testing is an essential phase i n the protocol development process. To ensure that each protocol implementation is able to inter operate w i t h other implementations correctly, conformance testing is applied to each implementation. There are many well known test methods which have been applied to protocol conformance testing w i t h varying degrees of success, such as U - , D - , W-methods [SD88, Gon70, Cho78]. E v e n though these methods have been improved and optimized [CVI89, V C I 8 9 ] , they still have a major shortcoming: they only address the control part of the protocols. T h e T E S T G E N environment overcomes this weak point by combining control flow testing and data flow testing i n test suite generation. This has been applied to some practical protocols successfully, such as the InRes, O S I class transport and L A P B protocols. T h e protocol T E S T suite Generation, selection, and validation E N v i r o n m e n t for conformance testing ( T E S T G E N + ) was developed at the University of B r i t i s h C o l u m b i a [Vuo93].  T h e overall functional structure of T E S T G E N + is described i n Figure 2.1.  There are three major modules: T E S T G E N , T E S T S E L and T E S T V A L for test suite generation, selection and validation respectively. TESTGEN  accepts protocol specifica-  tions i n a combination of Estelle.Y and A S N . l from the user.  T h e specifications are  converted to an internal data structure , Protocol D a t a Structure ( P D S ) , by the parsers.  4  Chapter 2.  TESTGEN+  Environment  5  USER  Estelle.Y + A S N . l Protocol Specification  Parsers  Constraints Editor  Protocol Data Structure  Test Suite c  Subtour  :  /  T S G Constraints  TESTGEN  {  TESTSEL  TESTVAL  internal files  Selected Test Suite  Legend: User accessible file Internal file  Validated Test Suite  I  I  C  )  Dynamic module  Figure 2.1: T E S T G E N +  Environment  Chapter 2.  TESTGEN+  Environment  6  It also accepts a set of user-defined constraints ( T S G constraints) through the constraints editor. T h e T E S T G E N tool obtains the protocol knowledge and the T S G constraints from the P D S , generates a test suite, and outputs the test suite i n the subtour form. The test suite can be fed into the TESTSEL  tool to get a refined test suite which has  the user acceptable cost and satisfied fault coverage. T h e test suite can also be fed into the TESTVAL  tool to check the validation of the test suite w i t h respect to the given  specifications.  2.1  Test Suite Generation -  TESTGEN  T E S T G E N is a major module i n T E S T G E N + .  T h e function of the T E S T G E N is to  generate test suites according to protocol specifications. T h i s module accepts protocol specifications i n A S N . l (for data), protocol specifications i n Estelle.Y (for control), and constraints, which can easily be edited by the user. It also generates test suite i n subtour, and two internal files for T E S T V A L and T E S T S E L respectively. T h e overall structure of T E S T G E N is depicted i n Figure 2.2. W i t h i n the T E S T G E N module, there are five modules: Estelle.Y parser, A S N . l parser, constraints editor, test suite generation engine and output module. In addition, there is one internal data structure, the P D S which contains all information obtained from both specifications. T h e modules' functions are given as follows: • Estelle.Y parser: This is a parser for the Estelle.Y language which is a modified subset of Estelle language, and is used to describe the control part of protocol specifications. T h e parser object is an internal data structure the P D S . • A S N . l parser: This is a parser for the A S N . l language which is used to describe the data part of protocol specifications. T h e parser object is an internal data structure  Chapter 2.  TESTGEN+  Environment  7  which is part of the P D S . • Constraints editor: T h e constraints editor module provides the user w i t h an i n teractive interface for definition of the T E S T G E N constraints.  In T E S T G E N ,  constraints are a set of boolean predicates that are used for the generation of each subtour. There are two types of constraints: (1) the m a x i m u m and the m i n i m u m usage conditions for all states, transitions, ISPs (Input Service P r i m i t i v e ) , O S P s (Output Service P r i m i t i v e ) , P D U s (Protocol D a t a U n i t ) , constants, variables, and Estelle.Y Specification  ASN.l Specification  ASN.l Parser  Protocol Data Structure  T S G Constraints  Constraints Editor  Test Suite Generation Engine  Output module  Subtours  Legend:  User accessible file Internal file  internal files  I  I  (  )  Functional module  Figure 2.2: T E S T G E N Structure  Chapter 2.  TESTGEN+  Environment  8  timers. (2) the parameter variations which include up to 10 values for each parameter of each ISP or P D U . T h e user can modify all of these constraints, save and restore the values, and set the default values through the editor. • Test suite generation engine: This module generates test suites based on the given specifications and a set of constraints.  T h e test suite is divided into test cases  which are subtours i n T E S T G E N . T h e subtour identification algorithm performs an exhaustive backtracking depth first search algorithm. It operates over the behavior tree representation of the protocol. E a c h subtour starts and ends at the same state, the initial state, and satisfies all the constraints conditions. These constraints l i m i t the length of each subtour. According to the protocol specification, only a finite number of the transitions can be applied i n each state. T h e parameter variation constraints on the parameters of the I S P and P D U l i m i t the number of different instances of the ISP and P D U i n the transition. Thus, the length and the number of different subtours are l i m i t e d if the backtracking algorithm is to finish successfully. E a c h subtour is recorded and saved into files through the output module. • Output module: This module is to save the test cases from the test suite generation engine into files. T h e test cases are i n subtour form, and two internal files used by the T E S T V A L and the T E S T S E L respectively.  2.2  Test Suite Selection -  TESTSEL  The function of T E S T S E L is to select test cases from the test suite output by T E S T G E N according to the user's requirement, such as cost and coverage tolerance, i.e., the number of test cases, and the distance between the test cases. This tool can accept test cases generated by T E S T G E N or other tools i n proper format which T E S T G E N can recognize,  Chapter 2.  TESTGEN+  Environment  9  and produce a subset of the test cases which satisfies the user. Test Suite  Filtering Module  Uniqued Test Suite  Parameters Value List  User  Selection Module  Selected Test Suite  Merge Module  Selected Test Suite  Figure 2.3: T E S T S E L Structure The overall structure of the T E S T S E L is i n Figure 2.3. W i t h i n the T E S T S E L m o d ule, there are three functional modules: filtering module, selection module and merging module. T h e i r functions are as follows: • Filtering module: This module strips off the data flow information from the test cases, leaving the control flow information i n the test cases as the output of filtering module. Complete test cases are composed of both control and data components. Test cases are filtered before being fed into the selection module because the selection module selects test cases based solely on the control component and not on both components.  Chapter 2.  TESTGEN+  Environment  10  • Selection module: This module selects test cases from the internal test cases which are the output of the filtering module arid produces a subset of test "cases by using the user defined constraints. These constraints are (1) the testing distance definition parameters pk and r^, (2) the test selection constraints including the m a x i m u m cost, the initial coverage tolerance e and m i n i m u m coverage tolerance e  m 4 n  which is the  test selection radius, (3) the radius scale factor for each pass. B y using a multi-pass algorithm, this module selects test cases to m a x i m i z e coverage subject to the cost constraint. It has been proven that all Cauchy sequences converge i n the metric space and repeated application of the greedy algorithm w i t h successively narrower test case radii produces such Cauchy sequences, thus, the greedy approach yields a set of test cases w i t h general coverage of the test suite and guarantees, convergence to the test suite. T h e test selection algorithm is guaranteed to yield a set of test cases which converge to the i n i t i a l test suite as more test cases are selected. This guarantees that no specific test cases are overlooked. A detailed algorithm can be found i n [MVC92] . • Merging module: This module accepts the subset test cases from the output of the selection module and merges the control component and the data component to form the final test cases. T h e selection module only processes the control components of test cases, hence only control information i n the output test cases is available. T h e data component of the test cases should be inserted to the control component to get the complete test cases for the user.  Chapter 2.  TESTGEN+  11  Environment  ASN.l Specification  Estelle.Y Specification  TESTGEN Parser  Protocol Data Structure  Preprocessor Module J  Test Cases  Validation Module  Output Module  Logging file  Legend: User accessible file Internal file Function module  Figure 2.4: T E S T V A L Structure 2.3  Test Suite Validation -  TESTVAL  T h e function of T E S T V A L is to check whether a given test suite is valid w i t h respect to a given Estelle.Y and A S N . l specification. Like T E S T G E N , T E S T S E L also accepts A S N . l specification and Estelle.Y specification, and gives out a logging file which contains the position of an event which is i n error of an indication the the test case is valid. T h e overall structure of T E S T V A L is given i n Figure 2.4. There are three functional modules: preprocessor module, validation module and output module. T h e i r functions are as follows:  Chapter 2.  TESTGEN+  Environment  .  12  • Preprocessor module: To process the test suite validation quickly and efficiently, this module converts some types of transitions i n the specification into a more suitable form for the validation module. It also translates the E F S M form of an Estelle.Y specification into a simple F S M form. • Validation module: This module validates given test cases w i t h respect to the P D S of the protocol specifications. • Output module: This module logs the traces of states and transitions which satisfy the given test cases i n a file. If a test case is valid according to the given formal specifications, a message - "test case valid" is i n the logging file. If a test case is invalid, the position is logged i n the file. B y using the information i n the logging file, errors i n test cases may be located.  Chapter 3  Estelle.Z Parser for T E S T G E N  3.1  Introduction T h e T E S T G E N tool accepts protocol specifications i n Estelle.Y for the control com-  ponent and specifications i n A S N . l for the data component of the protocol through two parsers. Hence, users need to learn both the A S N . l and Estelle.Y languages. O n the other hand, Estelle.Y is only a small subset of the Estelle language, and is not powerful enough to specify a real world protocol. Furthermore, the Estelle language is one of the most popular specification languages i n the real world. (Estelle, S D L and L O T O S are three common specification languages.) Therefore, it is necessary to expand E s t e l l e . Y + A S N . l into a large subset of Estelle or even to the whole Estelle language. A s a result of the T E S T G E N kernel accepting only the functions i n Estelle.Y and A S N . l , we have to define the Estelle.Z language which supports a l l functions i n E s t e l l e . Y + A S N . l , and can easily be expanded into the entire Estelle language. T h e output of the T E S T G E N tool is a set of subtours, which is easy to read for people, but not easily to be recognized by computers.  Hence, the T T C N (Tree and Tabular  Combined Notation) format is adapted for the T E S T G E N output. Also a graphic user interface is implemented. In this chapter, a description of the Estelle.Z language is presented briefly, followed by a discussion on the implementation of the Estelle.Z parser. A t the end, the improvement  13  Chapter 3.  Estelle.Z  Parser for  TESTGEN  14  of the interface of the T E S T G E N tool is discussed.  3.2  Estelle.Z Language Estelle.Z is a formal language defined to specify protocols for automatic test suite  generation. A n Estelle.Z specification is a modified, single module Estelle specification enhanced by introducing explicit language support for timers. A subset of the Estelle language is defined as Estelle.Z. T h e design goal is (1) to be easily expanded to the whole Estelle language; (2) to get an exact or very similar object data structure the P D S so that the T E S T G E N kernel can recognize the information i n the P D S ; (3) to follow the syntax of Estelle as closely as possible. T h e advantage of Estelle.Z is (1) users can specify protocols i n one language rather than two languages; (2) the syntax of Estelle.Z is more closer to Estelle than Estelle.Y; (3) the parser can be very easily expanded to complete Estelle language.  Syntax and Semantics T h e syntax of Estelle.Z is defined i n Backus-Naur F o r m ( B N F ) notation. A n Estelle.Z specification is a single module definition. It contains three components:  declaration,  initialization and transition. Variables and constants used i n the specification are defined in declaration component; the protocol state machine is initialized i n the initialization component; the transitions of the protocol state machine are defined i n the transition component. Declaration T h e declaration component contains constant declarations, variable declarations, channel declarations, timer declarations and state declarations. T h e syntax of variable and constant declarations is similar to that i n Pascal.  Chapter 3.  Estelle.Z  Parser for  TESTGEN  15  Estelle.Z language supports five data types for variables and constants:  integer,  boolean, character string, enumeration and record. Input Service P r i m i t i v e s (ISPs), Output Service P r i m i t i v e s (OSPs) and Protocol D a t a Structures ( P D U s ) are defined i n the channel declaration, these are necessary for the T E S T G E N kernel. Timeout values are declared for timers.  A l l states i n the protocol machine are  defined i n the state declaration. Figure 3.1 is an example of the declaration component.  Specification HomeAgent; CONST  mipMHauthExtAuth = 100 ; AdLifetime = 18000 ;  VAR  PduMessage : ( RegRequest, DeRegRequest, RegReply, Datagram, Advertisement); RegRequest:  record ipSourceAddr  : integer;  isDestAddr  : integer;  end ; identification : integer;  C H A N N E L SPchannel ( Net, Other) ; by Net: Junk ; by Other : Junk ; C H A N N E L PDUchannel ( pdu, another); by pdu : RegRequest; RegReply ; Datagram ; TIMER STATE  ad_timer  600;  R E G I S T E R E D , IDLE ;  Figure 3.1: E x a m p l e of the Declaration Component  Chapter 3.  Estelle.Z  Parser for  TESTGEN  16  Initialization T h e initial state of the protocol machine is defined by the initialization. In addition, all the variables may be assigned their i n i t i a l values i n the initialization, or given default values if not explicitly initialized. Figure 3.2 is an example of the initialization.  Transition T h e transition component contains a set of state transitions which define the start states, the end states, and the i n p u t / o u t p u t events.  1  T h e clause group  (including from, to, when, priority, and provided clauses) specify the present state and the next state of a transition, the sending and receiving of the SPs and P D U s , the priority, and the enabling predicate. A group of Pascal statements specify the action function. F i v e Pascal statements are supported: assignment statement, if statement, while statement and compound statement and output statement. Moreover, a set of timer statements are supported to specify the operations on the timers. If the enabling predicate is satisfied, an ISP or P D U is received, the protocol is in the right control state, and the transition has the highest priority among a l l transitions, then the transition is fired, and the protocol machine moves to the next state. Figure 3.3 is an example of a transition declaration, A complete example of specification for the home agent is i n A p p e n d i x C .  Chapter 3. Estelle.Z Parser for  TESTGEN  INITIALIZE TO  IDLE  BEGIN identification := 0 : careofAddr  := 0 ;  END ;  Figure 3.2: E x a m p l e of the Initialization Component TRANS  FROM TO  IDLE REGISTERED  PROVIDED ( RegRequest.mipMHauthExtSPI = mipMHauthExtSPI)  AND  (RegRequesLmipMHauthExtAuth = mipMHauthExtAuth) A N D ( RegRequest.mipIdentification > identification.) (RegRequest.ipDestAddr  =  AND  mipHomeAgent)  BEGIN RegReply.ipSourceAddr = RegReply.mipType  mipHomeAgent;  := 3 ;  RegReply.mipLifetime  := RegRequest.mipLifetime  - 1;  IF (bindno = 1 ) T H E N careofAddr := RegRequest.mipCOA E L S E careofAddl output  := RegRequest.mipCOA;  pdu.RegReply ;  END;  Figure 3.3: E x a m p l e of the Transition Component  Chapter 3.  3.3  Estelle.Z  Parser for  TESTGEN  18  Implementation of Estelle.Z Parser  3.3.1  Lexical Analysis of Estelle.Z  Lexical analysis for Estelle.Z is done by the lexical analyzer L E X . T h e lexical analyzer reads from the source program, and carves the source program into tokens. E a c h token can be treated as a single logical entity. Identifiers, keywords, constants, operators and punctuation symbols are typical tokens. T h e lexical analyzer returns to its caller a code for the token that it found. It also returns a token value i f the token is not a reserved word, punctuation, or operator, such as an identifier, integer and string. In a compiler implementation, lexical analysis and syntactic analysis are normally performed i n the same pass.  T h e lexical analyzer operates under the control of the  parser. T h e parser asks the lexical analyzer for the next token whenever the parser needs one. T h e n the lexical analyzer returns the token code and an applicable token value to the parser. In the lexical analyzer of Estelle.Z, a l l the reserved words, punctuation and predefine operators i n Estelle are included, even though they are not utilized i n Estelle.Z. Therefore, this lexical analyzer can be used without much modification when Estelle.Z is expanded to the whole Estelle language.  3.3.2  Syntax Analysis of Estelle.Z  T h e parser for Estelle.Z is generated by the syntactic analyzer tool Y A C C . T h e syntactic analysis checks that input tokens occurring according to the patterns that are permitted by the specification for the source language. Y A C C input is produced based on the B N F rules of Estelle.Z. Figure 3.4 depicts the process of Estelle.Z parser generation. T h e object of the Estelle.Z parser is generation of  Chapter 3. Estelle.Z  Parser for TESTGEN  19  syntax trees which store the syntactical information of the statements and expressions i n an Estelle.Z specification. T h e syntax trees are stored i n data structure the P D S , from which the T E S T G E N engine can obtain information to generate test suites.  f  \  Estelle.Z L E X source code >v  _  -  ^J^^Estelle.Z f  Parser^) — — -  PDS  'N  Estelle.Z Y A C C source code  Figure 3.4: Estelle.Z Parser Generation  In a syntax tree, the statements are represented as tree nodes.  For example, A n  assignment statement, variable-name := expression, is depicted i n Figure 3.5(a).  The  variable-name can be a simple variable name or be a parameter at the left-hand side of the assignment statement. T h e expression can be a tree of any expression on the right-hand side of the assignment statement.  Figure 3.5(b) shows an example of the  syntax tree of an assignment statement and its right-hand side expression. if  Similarly,  statements, while statements, c o m p o u n d statements and output statements are  converted into syntax trees stored i n the P D S . In addition, expressions are represented by syntax trees.  Declaration In the declaration section, variables, constants, channels, timers and° states are declared. T h e parser converts the information into key, name, type and value (if applicable)  Chapter 3.  Estelle.Z  Parser for  TESTGEN  variable-name  expression  (a)  RegReply.mipLifetime : =  RegRequest.milLifetime - 1  (b)  Figure 3.5: Syntax Tree of Assignment Statement which are then stored i n the P D S . For example, i n the constant declaration, mipMHauthExtAuth  = 100  is stored as i n Figure 3.6, where the key is an index into constants. key = 0 name = mipMHauthExtAuth type = I N T T Y P E val = 100  Figure 3.6: Structure of Constant Declaration  Chapter 3.  Estelle.Z  Parser for  21  TESTGEN  Variables, timers and states are processed i n the same way as constants. T h e channel declaration varies slightly from the above. There are two types of declarations, SPchannel and P D U c h a n n e l . SPchannel declares the ISPs and O S P s used i n the specification. P D U c h a n n e l declares the P D U s used i n the specification. T h e information on SPs and P D U s is necessary for the T E S T G E N engine. A l l of the information, such as the parameter's field name and type, is stored i n the P D S . For example, the P D U RegRequest is stored as i n Figure 3.7. T h e P D U type tree is a pointer pointing to the P D U ' s parameters including name, type and other features (if applicable).  Initialization T h e parser sets default initial values for all variables, parameters and timers if they are not explicitly initialized. T h e default value is 0 for those of integer type, false key = 0 name = RegRequest P D U type tree  1  •  univTag = integer field name =  ipSourceAddr  univTag = integer field name =  ipDestAddr  univTag = integer field name = mipMHauthExtAuth  Figure 3.7: Syntax Tree of Channel Declaration ( P D U )  for  Chapter 3.  Estelle.Z  Parser for  TESTGEN  22  those boolean type and the empty string for those of character string type. T h e initial state of protocol machine is assigned i n this part. Otherwise the first state i n the state declaration is assumed to be the initial state.  Transition T h e transition consists of a group of transition definitions. E a c h transition definition is identified by a key, which is stored i n the trans_key[] field of the starting state of that transition. T h e transition definition includes the from state, the to state, the input events, the enabling predicate, the priority and the action function which is a set of statements. This definition is converted into a syntax tree. Whenever the basic components such as variables, constants, parameters are referenced, their types and keys are stored. T h e leaf nodes of a syntax tree may be variables, constants, parameters and timer constructs. Figure 3.8 shows the syntax tree of the transition i n Figure 3.3. In this example, the transition is from the I D L E state to the R E G I S T E R E D state, the input event is RegRequest, the output event is RegReply, the enabling predicate is the boolean expression stored i n epred field, and the action function consists of 12 statements, which are linked respectively to their syntax by the keys and types.  3.3.3  Semantic Analysis  Semantic analysis is used to determine the type of expressions, to check that arguments are of types that are legal for an application of an operator, and to convert the statements into syntax trees stored i n the P D S . Semantic analysis is carried out during the syntax analysis phase.  Chapter 3.  3.3.4  Estelle.Z  Parser for  Structure of the  TESTGEN  23  PDS  The internal object of the parser is the P D S , based on which the T E S T G E N can generate test suites automatically.  T h e P D S is designed to represent the  kernel formal  protocol specifications based on Estelle.Z formalism i n a machine accessible form.  The  key = 1 name = from = IDLE to  REGISTERED  priority = 0 ipdu = RegRequest opdu = RegReply epred : (RegRequest.mipLifetime > 0) and (RegRequest.mipMHauthExtSPI = mipMHauthExtSPI) and (RegRequest.mipMHauthExtAuth = mipMHauthExtAuth) and (RegRequest.mipIdentification > identification) and (RegRequest.ipDestAddr = mipHomeAgent) efn  1 key = 1 nb of stmts  =12  stmt 0 kind = ASTMT key = 6 stmt 1 kind = ASTMT  RegReply .ipSourceAddr  key = 7  stmt 11 kind = IFSTMT key = 1  Figure 3.8: Syntax Tree of State Transition  mipHomeAgent  Chapter 3.  Estelle.Z  Parser for  TESTGEN  24  protocol specification saved i n the P D S w i l l be directly used for the subtours identification process which is the key process of automatic test suite generation.  Since T E S T G E N  is completely dependent on the data i n the P D S , it is essential to ensure that the P D S correctly represents the information of the protocol specifications i n order to generate test suites correctly. O n the other hand, it is also important for information i n the P D S to be easily accessed by T E S T G E N . In addition, the P D S can be used as an internal m e d i u m between the test suite engine and the protocol specification, i.e., the P D S can be the internal object of any specification language parser w i t h some modification if necessary, and the test suite generation engine can yield test suites based on the P D S as showed i n Figure 3.9. protocol specification in X language  PDS  Figure 3.9: Environment of the Parser The P D S is organized i n a way shown i n Figure 3.10. Using the Estelle.Z language, a protocol is described i n terms of several sets of components, such as states, variables, constants, channels, timers and transitions.  Some  protocol components are further described i n terms of other sets of protocol components.  Chapter 3. Estelle.Z  Parser for  25  TESTGEN  int init_state int nb_of_states  key  name  nb_of_tr  tr_key  min_use  man_use  pstate[0...] nb_of transitions  min_use key  name  from_st  to_st isp osp  osp2  ipdu  opdu  opdu2  epred  man_use efn  priority  ptrans[0...] nb_of_variables pvar[0...]  key  name  min_use  type  max_use  init_ival  init_bval  min_assigned  init_cstr  max_assigned  nb_of_constants pconst[0...]  key  name  type  int_val  bool_val  char_ptr  min"_use  max_use  nb_of_isps pisp[0...]  key  name  pco  isp_typetree  nb_of_pdus  key  name  pco  osp_typetree  nb_of_pdus  key  mane  pco  sent_in  pdu_key  min_use  max_use  nb_of_osps posp[0...]  pdu_key  min_use  max_use  nb_of_pdus ppdu[0...]  recv_in  pdu_typetree  min_use  mx_use  nb_of_timers ptimer[0...]  key  | name  | timeout_value ,| init_status | min_start [ max_start | min_stop [max_stop  nb_of_texprs ptexpr[0...]  key  name  timer  status  nb_of_efns pefn[0...]  key  name  key  name  nb_of_statements  stmt_kind  stmt_key  nb_of_cstmts pcstmt[0...]  nb_of_statements  stmt_kind  stmt_key  nb_of_astmts pastmt[0...]  key  name  key  name  left_kind  left  right_expr  nb_of_ifstmts pifstmt[0...]  bool_expr  stmt_kind  stmt  name  bool_expr  stmt_kind  stmt  name  timer  else_stmt_kind  else_stmt  nb_of_wstmts pwstmt[0...]  key  nb_of_tstmts ptstmt  key  timer_op  t_op_arg  nb_of_spparms pspparmfO...]  key  name  sptype  spkey t_enode_ptr  type  nb_of_cnsts  Figure 3.10: Protocol D a t a Structure  bool_cnst  int_cnst chat_cnst  Chapter 3.  Estelle.Z  Parser for  TESTGEN  26  For example, transitions may be described by enabling predicates, action functions, statements, etc. Each set of protocol components is defined by a structure i n the P D S . T h e definitions of the major structures:  states, transitions, variables, constants and state-  ments, are given briefly i n the following sections. State Structure definition State is defined to describe the control states of a protocol. F i v e fields are used to represent a state as depicted i n Figure 3.11a. STATE  TRANSITION  key  key  name  name  number of trans  from state  trans_key[0]  to_state  trans_key[l]  epred efn pnotity  trans_key[MAXTRANS-l]  isp osp  min_use max  osp2 ipdu  use  opdu opdu2 mm_use max  (a)  use  (b)  Figure 3.11: D a t a Structure of State i n the P D S  • key is an index into the pstate array.  T h e current state is the A:eyth state i n the  Chapter 3. Estelle.Z Parser for  TESTGEN  27  state declaration and may be referenced as pstatefkeyj. • name is the state's name. • number_of_trans indicates the total number of transitions possible from this state. • trans_key is an array storing the keys to the transitions which are possible from this state. • min_use, max_use indicate the limitations of the usage of the current state, i.e., passing the state at least min_use times and at most max_use times. These are not a part of the specification, but are T E S T G E N constraints edited by the users. A l l the transitions possible from the given state can be assessed consequently by looking up the trans Jcey[key] array. This is used for the subtours identification process in the test suite generation engine.  Transition Structure T h e transition  Definition  structure defines the state transitions of the protocol machine. Fields  are as shown i n Figure 3.11b. • key is the keyth state transition i n the transition declaration. • name is the name of the transition if applicable. • from_state. to_state indicate the beginning and ending states of the transition by the keys to the states. • epred, afn are keys to the enabling predicate and the action function associated w i t h this transition. • priority indicates the priority of the transition i f applicable.  Chapter 3.  Estelle.Z  Parser for TESTGEN  .  28  • min_use, max_use are the limitations that the transition can be used at least min_use times and at most max_use times. These are not a part of the specification, but are T E S T G E N constraints edited by the users. The data structure of variables and constants consists of key, name, type and value fields. charjval  T h e value may be an integer, boolean or string stored i n intjual, for constants, or stored i n initJval,  The statements consist of if statement, assignment  statement.  initjbval  and init-cstr  while statement,  booljval  and  for variables.  compound statement  and  T h e syntax trees of these statements are stored i n the P D S as  shown i n Figure 3.10, and the meaning of the fields are plainly indicated by the field name.  3.3.5  Testing for the parser  The accuracy of the P D S is very crucial to the test suite generation engine since the test suite generation engine completely depends on the information i n the P D S . Three verification mechanisms are used to verify the accuracy of a generated the P D S . P r i n t i n g the P D S The P D S can be saved into a text file, and can also be displayed interactively on the screen by the user. T h e user can check a l l the information i n the P D S by reading the text file or check a particular part, such as an expression or a statement, by displaying the expression or statement on screen through a set of printing functions. Since there is a parser of Estelle. Y + A S N . l which converts a protocol specification into a P D S , the two P D S s generated by the two parsers, the E s t e l l e . Y + A N S . l parser and the Estelle.Z parser, can be compared. One protocol can be specified i n E s t e l l e . Y + A S N . l , as well as i n Estelle.Z. T h e two P D S s should be similar i f the protocol specifications are  Chapter 3.  Estelle.Z Parser for  TESTGEN  29  equivalent. Consistency checking In T E S T G E N + , there is a set of consistency checking functions developed to check the consistency of the P D S after it has been generated. Theses functions can be used to check the P D S generated by the Estelle.Z parser. Test suite coverage checking B y feeding the two specifications, one i n E s t e l l e . Y + A S N . l and the other i n Estelle.Z, for the same protocol into their respective parsers, the same test suites should be generated. The existence of numerous test cases i n a test suite makes it difficult to compare the two test suites on an individual case by case basis. T h e test coverage tool is used to compare the coverage of the two test suites. If they are the same or very similar, then the P D S generated by the Estelle.Z parser is correct. In Chapter 5, the home agent protocol is specified i n both E s t e l l e . Y - f - A S N . l and Estelle.Z. T h e two specifications are applied to the T E S T G E N engine and two test suites are generated. T h e two test suites are fed into the test coverage tool and the same results obtained. This w i l l be discussed i n detail i n Chapter 5.  3.4  Improvement on the interface of T E S T G E N  O u t p u t in T T C N . M P  format  T h e output formats of T E S T G E N are subtours for people to read, and the internal files for T E S T V A L and T E S T S E L . None of them is standard output format that can be used outside T E S T G E N + . Therefore, it is necessary to provide a standard output for T E S T G E N + so that the T E S T G E N + tool can be widely used.  Chapter 3. Estelle.Z Parser for  TESTGEN  30  For this purpose, the T T C N . M P format, a standardized test notation, is provided. The Tree and Tabular Combined Notation ( T T C N ) was developed and standardized by the ISO (International Organization for Standardization) i n 1990, and is used for precise specification of abstract test suites [ISO]. The T T C N consists of two types of notations: the tree notation, used i n dynamic behavior descriptions to describe events which can occur as alternative responses to a previous event, and a tabular component, used to simplify the representation of all static elements.  T h e T T C N is i n two formats, a graphical form denoted T T C N . G R , and a  machine-processable  form  denoted T T C N . M P . T h e T T C N . G R is human readable and  understandable. T h e T T C N . M P is a packed format representation to allow more uniform and more efficient storage [Pro92]. Because T T C N is a standardized test notation and T T C N . M P is a packed representation and a machine processable format, the T T C N . M P is developed as a output module i n T E S T G E N + . This module obtains information from T E S T G E N and the P D S , organizes them i n T T C N . M P format, and writes them to a file.  A test suite consists of four sections: overview, declaration, dynamic and constraints as shown i n Figure 3.12. T h e overview section names the test suite and defines its context w i t h respect to the protocol standard and test method. T h e declaration section provides the name, type definition, range and comments for all of the objects that are referenced in the test suite itself. T h e constraints section specifies particular data values for P D U fields or A S P parameters as used i n a constrained test event i n the dynamic behavior section. These constraints are different from the constraints i n the T E S T G E N tool. T h e dynamic section comprises a set of test cases, the m a i n body of the abstract test suite including the test case library, the test step library and the default behaviors library.  Chapter 3.  Estelle.Z  Parser for  TESTGEN  31  SUITE  ASP  PDU  CONSTANT  PCO  TIMER  VAR  Testcase  Testcase  ...  Testcase  Constraints from T E S T G E N  Figure 3.12: Architecture of T T C N Tree F r o m T E S T G E N A collection of test cases for the home agent i n T T C N . M P format is shown i n A p pendix F .  G r a p h i c a l user interface In order to give users a user friendly interface, a graphical user interface is provided based on the menu driven user interface. T h e graphical user interface is implemented on X V i e w library under SunOS U N I X 4.1.3.  Under this user interface, T E S T G E N ,  T E S T S E L and T E S T V A L are integrated under T E S T G E N + , so that the user can easily travel among the three tools simply by clicking on the mouse. T h e function of the graphical user interface is the same as the menu driven user interface for T E S T G E N , T E S T S E L and T E S T V A L . In addition, some items are added to enhance the T E S T G E N menu, such as storing the constraint instances and parameters of P D U s , ISPs and O S P s , removing the subtours file when restarting the T E S T G E N tool, choosing to display the default constraints, editing the subtours file and T T C N . M P file, etc.  Chapter 3.  3.5  Estelle.Z Parser for  TESTGEN  32  Summary  In this chapter, the Estelle.Z parser has been presented.  T h e Estelle.Z parser accepts  the Estelle.Z specification language, and produces a representation of the protocol as a P D S . the object structure of T h e lexical, syntactic and semantic analyses of the parser have been discussed. In chapter 5, a real world protocol specification i n Estelle.Z w i l l be fed i n the parser to test its accuracy.  Chapter 4  Specification of a Subset of the M o b i l e IP Protocol  Introduction T h e M o b i l e I P Protocol, also called I P M o b i l i t y Support, is an Internet-Draft subm i t t e d by the M o b i l e IP Working Group of the Internet Engineering Task Force ( I E T F ) , to route IP datagrams transparently i n the Internet. Version 15 of this protocol released i n February, 1996 [Per96] is discussed i n this thesis. In the M o b i l e IP Protocol, each mobile node is identified by its home I P address, regardless of where the mobile node's current point of attachment to the Internet is. If a mobile node is away from its home network, then it is associated w i t h a care-of address which provides information about its current point of attachment to the Internet. T h e mobile node then registers the care-of address w i t h its home agent.  T h e home agent  sends datagrams headed for the mobile node through a tunnel to the care-of address. A t the end of the tunnel, each datagram is either directly delivered to the mobile node or is delivered v i a a foreign agent. In this chapter, the basic concepts and functions of the M o b i l e I P Protocol are described. One major element, the home agent, is discussed i n detail. T h e formal specification of the home agent is presented.  33  Chapter 4.  Specification  of a Subset of the Mobile IP  Protocol  34  User ( T C P )  Advertisement  RegReply FA  '.IP/Mobile IP  Router  foreign network  Net (Link)  Note:  *  H A : Home Agent  *  F A : Foreign Agent  *  M H : Mobile Host  Figure 4.1: M o d u l e of M o b i l e IP 4.1  Basics of the P r o t o c o l There are three major modules i n the mobile IP protocol: (1) Home Agent, (2) Foreign  Agent and (3) Mobile Host or M o b i l e Node as shown i n Figure 4.1. The home agent is a router on the mobile node's home network. W h e n a mobile node is away from its home, the home agent maintains information on its current location and tunnels datagrams to the mobile node. The foreign agent is a router on the mobile node's foreign network. W h e n a mobile node is registered w i t h a foreign agent, the foreign agent provides routing services to the mobile node. The mobile host is a host or a router which can change its point of attachment from one network to another. A mobile host may change its location without changing its IP  Chapter 4. Specification  of a Subset of the Mobile IP Protocol  35  address and may continue to communicate w i t h other Internet nodes by using this IP address. In the following subsections, an overview of the M o b i l e I P protocol is given and the functions of the three modules are discussed.  4.1.1  Protocol  Overview  M o b i l e I P protocol provides two types of services: 1. Agent Discovery: T h e home agent and the foreign agent advertise their services on the subnetworks where they are available. B y listening to these advertisements, a newly arrived mobile node can locate a foreign agent i f it is i n a foreign network, or a home agent i f it is i n its home network. 2. Registration: W h e n a mobile node is away from its home, it registers its care-of address w i t h the home agent. If the mobile node can find a foreign agent i n the current network, then the foreign agent's I P address w i l l be the care-of  address  and the mobile node can register w i t h its home agent through the foreign agent. Otherwise, the mobile node can get a co-located care-of address, a temporary or a long-term address used by the mobile node while visiting the foreign network, by some external assignment mechanism, and register this temporary address w i t h its home agent directly.  T h e M o b i l e IP Protocol operates i n the following manner: • T h e foreign agent and the home agent advertise their presence by sending an Agent Advertisement message.  Chapter 4.  Specification  of a Subset of the Mobile IP  36  Protocol  • A mobile node analyzes the Agent Advertisement messages it receives and assesses whether it is on its home network or on a foreign network. If the mobile node is on its home network, it operates without mobility service. If it is returning to its home network from a foreign network, the mobile node de-registers w i t h its home agent by sending a Registration Request and receiving a Registration Reply. If the mobile node moves to a foreign network, it registers its new care-of address w i t h its home agent by sending a Registration Request and receiving a Registration Reply either directly or through a foreign agent. • Datagrams delivered to the mobile node's home address are intercepted and tunneled by its home agent to the mobile node's care-of address.  T h e y are then de-  livered to the mobile node by a foreign agent or tunneled to the mobile node's co-located care-of address, i.e., the mobile node. • Datagrams sent by the mobile node are generally delivered to their destinations by using standard I P routing mechanisms, and not by using any mobility services.  4.1.2  H o m e Agent  T h e services provided by the Home Agent are: • Agent Advertisement: T h e home agent advertises its services on a link by sending Agent Advertisement messages periodically. T h e mobile nodes use these advertisements to determine their current point of attachment to the Internet, i.e., whether they are on their home networks. A n Agent Advertisement is an I C M P (Internet Control Message Protocol) Router Advertisement that has been extended to also carry a M o b i l i t y Agent Advertisement Extension.  Chapter 4. Specification  of a Subset of the Mobile IP Protocol  37  • Registration: T h e home agent receives Registration Requests, processes them and sends Registration Replies to grant or deny the services requested. If service permission is granted, then the home agent w i l l update its mobility binding list w i t h the care-of address of the tunnel and send the registration reply w i t h an appropriate message. If the registration request is denied, then the home agent w i l l send the Registration Reply w i t h a suitable error code. If the parameter life-time i n the Registration Request is zero, then the home agent w i l l de-register the current care-of address.  B y maitaining the binding list, the home agent can serve more  than one mobile nodes. • Routing: T h e home agent intercepts a l l the datagrams on the home network that are addressed to the mobile node while the mobile node is registered away from its home. If the IP Destination Address of the arriving datagrams is the same as the home address of the mobile node, then the home agent tunnels the datagrams to the mobile node's currently registered care-of address. If the mobile node has no current mobility bindings, i.e., it is at home, and the home agent is also a router handling common IP traffic, then the home agent w i l l forward the datagram directly to the mobile node. If the mobile node requires, then the home agent w i l l forward the broadcast messages to the mobile node.  4.1.3  Foreign Agent  The foreign agent supports the following services: • Agent Advertisement: Similar to the home agent, the foreign agent advertises its services on a link by sending Agent Advertisement messages periodically to the local network. T h e foreign agent uses different parameters from that of the home  Chapter  4.  Specification  of a Subset of the Mobile IP  Protocol  38  agent, including the foreign agent's care-of address for the mobile nodes. T h e careof address usually is the IP address of the foreign agent. • Registration: W h e n a mobile node registers w i t h its home agent v i a a foreign agent, the foreign agent only relays valid Registration Requests between the mobile node and the home agent and valid Registration Replies between the home agent and the mobile node.  Each foreign agent maintains a visitors' entry list containing  the information obtained from the mobile node's Registration Requests.  When  the foreign agent receives a valid Registration Reply from the home agent, hence indicating a successful Registration, the foreign agent modifies the visitors' entry list. B y maintaining the visitors' entry list, the foreign agent can serve more than one visiting mobile nodes. • Routing: The foreign agent receives datagrams sent to its advertised care-of address. If the datagrams are destined for its visiting mobile nodes, then the foreign agent forwards the datagrams to these mobile nodes, otherwise it discards them.  4.1.4  M o b i l e Host  A mobile host, also called a mobile node, has the following functions: • Agent Discovery: After a mobile node receives an Agent Advertisement, it can determine whether it is on its home network or on a foreign network. If the mobile node returns to its home network from a foreign network, it de-registers w i t h its home agent directly. If the mobile node moves to a foreign network, it registers w i t h its home agent v i a a foreign agent, which is sending an Agent Advertisement w i t h a care-of address. If the mobile node does not receive any Agent Advertisement for a certain amount of time, and if it can obtain a care-of address through a link-layer  Chapter  4.  Specification  of a Subset of the Mobile IP  Protocol  39  protocol or other means, then the mobile node registers the care-of address w i t h its home agent directly. Otherwise, the mobile node sends an Agent Solicitation to search for an agent. • Registration: A mobile node initiates a registration whenever it detects a change in its network connectivity. W h e n it is away from its home, the mobile node's Registration Request allows its home agent to create or modify a m o b i l i t y binding for the mobile node. W h e n it is at home, the mobile node's (de)Registration Request allows its home agent to delete any previous m o b i l i t y binding(s) to it. A mobile node is able to operate without the support of m o b i l i t y functions when it is at home. After sending a Registration Request, the mobile node w i l l receive a Registration Reply, either from a home agent or a foreign agent. If the registration is accepted, then the mobile node configures its routing table accordingly. If the registration is rejected, then the mobile node modifies its Registration Request according to the error information on the Registration Reply, and tries again. • Routing: W h e n a mobile node is connected to its home network, it operates as a stationary host.  W h e n it is registered on a foreign network, the mobile node  chooses a default router. If it is registered w i t h a foreign agent, the foreign agent becomes the default router, otherwise, the local network router becomes the router.  4.1.5  Example  In this section, an example is given to show how the mobile IP protocol functions. In Figure 4.2 (a), the mobile node moves into a foreign network and detects a foreign agent. The mobile node sends a Registration Request to the foreign agent (1), the foreign  Chapter 4. Specification  of a Subset of the Mobile IP  Protocol  40  agent relays the request to the mobile node's home agent(2). If the request is accepted, the home agent sends a Registration R e p l y to the foreign agent(3), and the foreign agent  >-  home agent  4  foreign agent •<•  1  foreign network  hust  (a)  home agent  2 •'  >-  mobile node  router  foreign network lliM  (b) Legend:  Data sent from mobile node Data send to mobile node Registration Request/Reply  Figure 4.2: E x a m p l e of mobile I P Operation  mobile node  Chapter 4. Specification  of a Subset of the Mobile IP Protocol  41  relays the request to the mobile node(4). If a message is sent to the mobile node, the home agent intercepts the message and tunnels it to the foreign agent. Subsequently, the foreign agent forwards the message to the mobile node after checking i f the message is for the mobile node who is visiting the local network (dashed line). If a message is to be sent from the mobile node, it is first sent to the foreign agent and then to the destination host v i a normal I P routing methods (dotted line). In Figure 4.2 (b), a mobile node moves into a foreign network where no foreign agent is presently implemented. T h e mobile node obtains a co-local care-of address, and registers w i t h its home agent d i r e c t l y ( l ) . If the request is accepted, the mobile node receives a Registration Reply from the home agent(2).  If a message is to be sent to the mobile  node, the home agent tunnels it to the mobile node (dashed line). If a message is to be sent from the mobile node, it is initially directed to the local router and then delivered to the host (dotted line). T h e home agent is discussed more thoroughly i n the next section.  Chapter 4. Specification  4.2  of a Subset of the Mobile IP Protocol  42  H o m e Agent T h e home agent is one of the most important elements i n mobile IP protocol. It is  necessary to discuss the messages received or sent by the home agent to fully understand its behaviors. T h e home agent receives one k i n d of message, Registration Request, and sends two kinds of messages, Registration R e p l y and Agent Advertisement. T h e home agent also receives and forwards datagrams. These datagrams are I P datagrams, therefore they are not discussed i n this thesis. Table 4.1 shows the major fields i n Registration Request:  Field 1  2  3  4  5  Name  Description  Source Address Destination Address Type Lifetime Home address Home agent Care-of address Identification  address from which the message is sent address of foreign agent or the home agent 1 the life time for this request IP address of the mobile node IP address of the mobile node's home agent IP address of the end of tunnel constructed by mobile node  Type SPI Authenticator  32 Security Parameter Index message authentication code  Type SPI Authenticator Type SPI Authenticator  33 Security message 34 Security message  Parameter Index authentication code Parameter Index authentication code  Table 4.1: Fields i n Registration Request  Required  V V V V V V V V V V  Chapter 4.  Specification  of a Subset of the Mobile IP  Protocol  43  There are five fields i n this table: field one is the IP field which indicates the source and destination addresses of the message; field two is the UDP field which indicates information about the mobile node; field three is the Mobile-Home  Authentication  Ex-  tension which indicates the authentication between a mobile node and its home agent. These three fields are essential i n the Registration Request message. Mobile-foreign  Authentication  Extension,  F i e l d four is the  which indicates the authentication between a  mobile node and a foreign agent i n the foreign network, if applicable. F i e l d five is the Foreign-Home  Authentication  Extension,  which indicates the authentication between the  mobile node's home agent and a foreign agent, i f applicable. In some networks, there is no implementation of a foreign agent. Thus, there is no authentication related to the foreign agent. Hence the last two fields are optional. Table 4.2 shows the major fields i n Registration Reply: Field 1  2  3  4  5  Name  Description  Source Address Destination Address Type Code Lifetime Home address Home agent Care-of address Identification  address from which the message is sent source address of Registration Request 3 0/1 for success, others for error code the life time for this request IP address of the mobile node IP address of the mobile node's home agent IP address of the end of tunnel based on the Identification of Registration Request  Type SPI Authenticator Type SPI Authenticator Type SPI Authenticator  32 Security message 33 Security message 34 Security message  Parameter Index authentication code Parameter Index authentication code Parameter Index authentication code  Table 4.2: Fields i n Registration R e p l y  Required V V V V V V V V V V  Chapter 4. Specification  of a Subset of the Mobile IP Protocol  44  Similar to the fields i n Registration Request, there are five fields i n Registration Reply. T h e first two fields are related to IP field and UDP field. T h e difference between a Registration Request and a Registration Reply is the code field which indicates the registration result. T h e code is 0 or 1 i f the registration is successful, otherwise, the code is a number (greater than 1) indicating an error message. T h e last three fields are similar to the fields i n the Registration Request i n that they indicate the authentication among the mobile node, the home agent and the foreign agent. Table 4.3 shows the major fields i n an Advertisement:  Field  Name  Description  1  Destination Address  link layer destination address  2  TTL Destination Address  time to live, set to 1 IP address of local broadcast address  Lifetime H Type Sequence number Registration lifetime  the life time for this Advertisement set to 1 if it is a home agent 16 integer m a x i m u m of acceptable seconds  3  _ Required  V V V V V V V  Table 4.3: Fields i n Advertisement  There are three fields i n Agent Advertisement: link-layer field, to indicate the destination; IP fields, to indicate T i m e To Live of the message; and Mobility Agent Extension,  Advertisement  to indicate that an I C M P Router Advertisement message is also an Agent A d -  vertisement being sent by a mobility agent for additional information about the mobility service that the agent supports. T h e I P M o b i l i t y Support documentation[Per96] gives more detailed information on each message communicated between the mobile node, the home agent and the foreign  Chapter 4. Specification  of a Subset of the Mobile IP Protocol  45  agent.  4.3  T h e formal Specifications of the H o m e Agent F r o m the above sections, we have acquired more knowledge about the home agent.  Based on this knowledge, we can discuss the formal specification of the home agent, which is used by the test generation tool ( T E S T G E N ) to generate test cases. To simplify the specification, one mobile node is assumed. T h e T E S T G E N tool accepts specification i n A S N . l for the data part and specification i n Estelle.Y for the control part, or specification in Estelle.Z for both parts.  D a t a Part in A S N . l The corresponding protocol data units ( P D U s ) received or sent by the home agent and their basic parameters are as follows: • RegRequest : Registration Request. To simplify the specifications, only 11 major parameters are presented as follows: Name  Typ  D e s c r i p t i o n / Meaning  e  IP f i e l d s ipSourceAddr  INTEGER  addr. from which the message i s  ipDestAddr  INTEGER  addr. of f o r e i g n agent / home agent  Mobile IP f i e l d s mipType  INTEGER  set  mipS  INTEGER  1: simultaneous bindings  mipLifetime  INTEGER  time remaining before  to 1  expired  sent  Chapter 4. Specification  of a Subset of the Mobile IP  Protocol  mipHomeAddr  INTEGER  IP addr. of mobile node  mipHomeAgent  INTEGER  IP addr. of mobile node's home agent  mipCOA  INTEGER  IP addr. of the end of the tunnel  mipldentification  INTEGER  number constructed by the mobile node  — Mobile-Home Authentication Extension mipMHauthExtSPI  INTEGER  Security Parameter Index (4 Bytes)  mipMHauthExtAuth  INTEGER  Authenticator, keyed MD5  • RegReply : Registration Reply. To simplify the specifications, only 10 parameters are presented as follows: Name  Type  Description / Meaning  IP f i e l d s ipSourceAddr  INTEGER  addr. from which the message i s  ipDestAddr  INTEGER  addr. of foreign/home  sent  agent  Mobile IP f i e l d s mipType  INTEGER  set to 3  mipCode  INTEGER  the r e s u l t of r e g i s t r a t i o n request  mipLifetime  INTEGER  time remaining before  mipHomeAddr  INTEGER  IP addr. of mobile node  mipHomeAgent  INTEGER  IP addr. of mobile node's home agent  mipldentification  INTEGER  number constructed by the mobile node  expired  — Mobile-Home Authentication Extension mipMHauthExtSPI  INTEGER  mipMHauthExtAuth  INTEGER  Security Parameter Index (4 Bytes) Authenticator, keyed MD5  Chapter 4. Specification  of a Subset of the Mobile IP  Protocol  47  • Advertisement : Agent Advertisement. To simplify the specifications, only 6 parameters are presented as follows:  Name  Type  —  D e s c r i p t i o n / Meaning  IP f i e l d s  ipDestAddr  INTEGER  multicast addr. or l i m i t e d broadcast addr.  ipTTL  INTEGER —  IP f i e l d , must be set to 1  ICMP f i e l d s  icmpLifetime  INTEGER  l i f e time of v a l i d advertisement i n t e r v a l = 1/3 l i f e t i m e  icmpCode  INTEGER —  0: as a router too  M o b i l i t y Agent Advertisement Extension  extRegLifetime  INTEGER  longest time acceptable of r e g i s t r a t i o n .  extH  INTEGER (0..1)  1: t h i s i s a home agent  A p p e n d i x A contains the complete A S N . l specification for the simplified home agent. A p p e n d i x D contains the A S N . l specification for a l l the parameters i n all P D U s .  Chapter 4. Specification  of a Subset of the Mobile IP  Protocol  48  Control Part in E s t e l l e . Y and Estelle.Z The Extended F i n i t e State Machine ( E F S M ) of the home agent is shown i n Figure 4.3.  +timer[l/3 Ad.LT]/-Advertisement  RegReq(Reg.LT > 0 & & valid)/-RegRep(OK)  +RegReq(invalid)/-RegRep(errcode) +timer[l/3 Ad.LT]/-Advertisement  +RegReq(Reg.LT = 0 & & validV-RegRep(dereg) +Datagram/-Datagram(binding = 0)  +RegReq(valid)/-RegRep(OK) +Datagram/-Datagram (binding = 1)  +RegReq(invalid)/-RegRep(errcode)  Note: RegReq : Registration Request R e g R e p : Registration Reply dereg State: I D L E , R E G I S T E R E D  : deregistration  errcode : error code R e g . L T : life time in Registration Request Ad.LT  : life time in Advertisement  Figure 4.3: E F S M of the Home Agent  Chapter 4. Specification  of a Subset of the Mobile IP Protocol  49  T h e E F S M has 2 states, I D L E and R E G I S T E R E D , which are defined as follows: 1. I D L E : Initial state. A t h e the beginning, the home agent is awaiting the Registration Request from the foreign agent, the mobile node, or the datagrams from networks, while the home agent sends Agent Advertisement periodically. W h e n the home agent receives a Registration Request, it checks its validity. If it is invalid, it sends a Registration Reply w i t h a related error code and it remains at a I D L E state; i f it is valid, it sends a Registration R e p l y w i t h a successful code and transfers to a R E G I S T E R E D state; i f datagrams are received, the home agent discards them as the mobile node has not been registered yet. 2. R E G I S T E R E D : W h e n a Registration Request is accepted, the home agent moves to this state, which means that it provides mobility service to the mobile node from now on. If datagrams are received while i n this state, the home agent tunnels them to the care-of address of the mobile node; if another Registration Request is received, and if the home agent supports simultaneous bindings, then the home agent registers the mobile node w i t h another care-of address; if a de-Registration Request is received, then the home agent checks its validity, if it is valid, then it de-registers for the mobile node. A t the same time, the home agent sends Agent Advertisement periodically. W h e n receiving P D U s or internal events, such as timeouts, the home agent may change its state or remain i n its current state, and send corresponding P D U s .  State transmissions are described as follows: • from I D L E to I D L E : 1. receive Registration Request (invalid), reply w i t h error code  Chapter  4.  Specification  of a Subset of the Mobile IP  Protocol  50  2. receive Datagrams for non-registered mobile node, discard 3. send Agent Advertisement periodically (time out) • from I D L E to R E G I S T E R E D — receive Registration Request (valid ), reply w i t h 0/1 code • from R E G I S T E R E D to I D L E - receive Registration Request (Lifetime = 0, valid), reply w i t h 0/1 code • from R E G I S T E R E D to R E G I S T E R E D 1. receive Registration Request (valid), reply w i t h corresponding code 2. receive Registration Request (invalid), reply w i t h corresponding error code 3. receive Datagrams for mobile node (if it is i n a foreign network), tunnel the Datagram 4. receive Datagrams for mobile node (it is i n its home network), deliver the Datagram 5. send Agent Advertisement periodically (time out)  The complete specification i n E s t e l l e . Y is given i n A p p e n d i x B . The complete specification i n Estelle.Z is given i n A p p e n d i x C .  Chapter 5  A p p l y i n g M o b i l e IP to T E S T G E N  Introduction In chapter 3, the new parser was described. In chapter 4, the specifications of the M o b i l e IP protocol were presented. In this chapter, the specifications of the M o b i l e I P are fed into the T E S T G E N tool to yield test cases i n order to determine whether the new parser functions correctly. Hence, we can compare the two sets of test cases yielded from the two parsers. Since the number of test cases is too large, and there is extreme data variation i n the test cases, we fed those test cases into the T E S T S E L tool to test their coverage and other features. In this chapter, the quality of test cases generated by T E S T G E N is discussed, followed by a discussion on the coverage of test cases. Comments on the two parsers are summarized at the end of this chapter.  5.1  T h e Test Suite Generation W h e n a protocol is implemented, we need to test if it has been implemented consis-  tently w i t h its specification and if it can cooperate w i t h existing networks smoothly, i.e., we need to apply conformance testing to the implementation. T E S T G E N is one tool that allows the generation of various test cases to check the reaction of the implementations. In this section, the algorithm of T E S T G E N is given succinctly [LV93], followed by the constraints chosen for the testing of the M o b i l e I P protocol.  51  Chapter 5. Applying  5.1.1  Mobile IP to  52  TESTGEN  T h e A l g o r i t h m of T E S T G E N  Before we introduce the algorithm of T E S T G E N , let's first define two terminologies that w i l l be used later. 1. A n extended transition system ( E T S ) is a quadruple ETS • Q = States x Variables  x Constants  x Timers,  = (Q, E, —>•, qi it) • n  denoting the set of states  of the E T S . • E = ISP  U OSP  • ->Q Q x E x Q,  U PDU,  denoting the set of events of the E T S .  denoting the transition relation for the E T S .  • Qinit £ Q-, denoting the i n i t i a l state of the E T S . 2. Subtour (X, Si, So, C)  is the set of all executable paths (subtours) from an i n i t i a l  state Si to a final state So, where So is the i n i t i a l state of a finite state machine X w i t h constraint C .  In T E S T G E N , Si = So, because the test control sequences  begin and end at the same initial state So (is usually idle). T h e constraint C is a set of feasible paths, including restrictions on the iteration number of while loops and transition loops, etc.. T E S T G E N generates subtours (test cases) based on a set of constraints and the information i n the P D S which has been established by the parsers according to a given specification. T h e subtours generation algorithm is an exhaustive depth first search over the protocol behavior tree. If a test branch of this tree fulfills all the defined constraints, then a subtour is identified w i t h this test branch. follows:  T h e algorithm is given briefly as  Chapter 5. Applying  Mobile IP to  Generate_subtour( E T S , C ,-„, m  C  m a  53  TESTGEN  x,  q, u , subtour)  { find transition t i n the E T S that can be fired at state q; for each t  {  i f the event of t is an I S P or I P D U (Input P D U ) { for a l l ISP or I P D U parameter value combination v G CV i f t is enabled by v  {  apply action function to state q and event ( I P D U or I S P ) ;  Qnext  ^~ u-\- the elements usage of action function of t  Unext  subtour  <r- subtour + (t,v);  next  if  {  C i m  5; ^next 5: C ax  n  m  and (Jnext — Qinit  { output the subtour to the file; return; } if u t  ^  nex  C  max  Generate_subtour ( E T S , C  m j n  , C  m a x  ,  <j ext i nexti u  n  subtour  } } }; if  the event of i is a P R O V I D E D clause and no W H E N clause { i f t is enabled  apply action function to state q;  Qnext  ^— u+ the the elements usage of action function of t  Unext  subtour  next  if  C i m  {  n  «— subtour + (t,v); ^ U  n e x  t  ^ C  max  and  ([next — (Jinit  );  next  Chapter 5. Applying  Mobile IP to  TESTGEN  54  { output the subtour to the file; return; } if u."next  < c,  — max  Generate_subtour ( E T S , C  m t r i  , C,  subtour. nextj i  } } } } where C  max  is a vector of all the m a x i m a l constraints, C i  m n  is a vector of a l l the m i n i m a l  constraints, q is a state, u is a vector of the number of current usages for a l l parameters, CV  is a set of a l l allowed parameter value combinations. Using the algorithm above, subtours that satisfy the constraints can be generated.  The algorithm generateds finite subtours, because of the restriction of the constraints.  5.1.2  Constraints of T E S T G E N  There are two types of constraints i n T E S T G E N . One type sets the m a x i m u m and m i n i m u m usage for all elements, including states, ISPs, O S P s , P D U s , constants, variables, and timers. T h e other type is the parameter variations which define a set of values for all ISPs and P D U ' s parameters. In addition, there is a set of default constraint values set by T E S T G E N . T h e default values for all m a x i m u m and m i n i m u m usage of a l l elements are 1 and 0 respectively, and for parameter variations are 0 and 99 respectively. W i t h the default constraint values, 2053 test cases are generated from the home agent specification. T h e 2053 test cases come from 3 test control sequences w i t h data variation: (1) I D L E to I D L E with P D U Advertisement; (2) I D L E to I D L E w i t h P D U Datagram and no output; (3) I D L E to I D L E w i t h no meaningful P D U RegRequest and RegReply.  Chapter 5. Applying  Mobile IP to  TESTGEN  55  T h e reason is that the m a x i m u m usages of a l l parameters are set to 1 and the m i n i m u m usages of all parameters are set to 0, the values of P D U parameters are set to 0 and 99. Such values are not meaningful i n the home agent protocol. We modify the constraints value i n the following way: state R E G I S T E R E D is passed at least once and at most 3 times; state I D L E is passed at least once and at most twice. Hence the mobile node can apply for registration, get the service of data transmission and advertisements from home agent, and apply for de-registration. T h e values of P D U parameters are set according to the meaning of the parameters and the testing purpose. It is necessary to test the validation of the Registration Request according to specification, so both the correct and incorrect parameter values for the'Registration Request's parameters are supplied, including m i p M H a u t h E x t S P I and m i p M H a u t h E x t A u t h , etc.. A l l the ISPs and O S P s ' parameters are set to 0, because these ISPs and O S P s are not utilized i n our testing, but they are required by the grammar of the specification. T h e major m i n . and max. constraint values and the major parameter variation constraints of P D U s i n the M o b i l e IP protocol are given as follows: 1. State I D L E (1/2) R E G I S T E R E D (1/3) 2. Transitions For all transitions (0/99) 3. ISP For a l l ISPs (0/0) 4. O S P For a l l O S P s (0/0)  Chapter 5. Applying  Mobile IP to  TESTGEN  The following are the major parameter variation constraints for P D U s : 1. RegRequest ipSourceAddr ( 8285 ) i p D e s t A d d r ( 821045, 82832 ) mipType ( 1 ) mipS ( 1 ) mipLifetime ( 10 ) m i p H o m e A d d r ( 821012 ) mipHomeAgent ( 821045 ) m i p C O A ( 821020 ) mipldentification ( 5, 20 ) m i p M H a u t h E x t S P I ( 200, 250 ) m i p M H a u t h E x t A u t h ( 100, 150 ) 2. DeRegRequest ipSourceAddr ( 821012 ) i p D e s t A d d r ( 821045 ) mipType ( 1 ) mipS ( 1 ) m i p H o m e A d d r ( 821012 ) mipHomeAgent ( 821045 ) mipCOA ( 0 ) mipldentification ( 50 ) m i p M H a u t h E x t S P I ( 200 )  56  Chapter 5. Applying  Mobile IP to  TESTGEN  57  m i p M H a u t h E x t A u t h ( 100 ) 3. Advertisement For all parameters ( 1 ) 4. RegReply For a l l parameters (1 )  A l l the parameters of Advertisement and RegReply are assigned i n the protocol specification, so the values i n the constraint part are initialized to 1. This does not affect the test case generation. W i t h the above constraint values, there are 641 test cases generated by T E S T G E N which come from 4 test control sequences w i t h data variation. T h e 4 typical test control sequences and the typical test cases i n T T C N . M P form are given i n A p p e n d i x F . If I D L E (1/2) is changed to I D L E (1/3), there w i l l be 27802'test cases. These test cases are to be used i n the T E S T S E L later.  5.1.3  C o m m e n t s on  TESTGEN  W i t h the experience of utilizing T E S T G E N on M o b i l e IP, m y experience and comments on T E S T G E N are as follows:  Advantages: 1. B y using formal specification, Estelle.Y and A S N . l or Estelle.Z, the ambiguities i n the specification written i n English can be detected earlier. 2. It is convenient for the user to have various choices through T E S T G E N menus to select different parameter constraints according to the testing purposes. A l s o , it is  Chapter 5.  Applying  Mobile IP to  TESTGEN  58  easy to repeat the operation u n t i l the user gets a satisfactory result. 3. T E S T G E N combines both the control component and the data component, therefore it can yield many different instances for test cases. In the real testing, there may be a l l kinds of messages fed into the implementation. For example, i n the home agent implementation, a RegRequest w i t h different parameters may be received. F r o m T E S T G E N the instances of such RegRequest can be generated.  Problems i n T E S T G E N : 1. Assignment statement: Sometimes the assignment statements i n the specification are not executed correctly. For example, a l l the parameters of RegReply P D U are assigned i n the specification according to the test purpose, but the subtours generated by the T E S T G E N reveal values which are not assigned i n the specification, such as - 1 , 99 and so on. These parameter values of RegReply render the subtours meaningless. For the Advertisement P D U , the parameters are correctly assigned as the values i n the specification. 2. P r o v i d e d statement: Sometimes the provided statements are executed incorrectly. For example, when conditions are satisfied, the F S M should transform from state R E G I S T E R E D to state I D L E , however it does not. Hence, it is necessary to add one more P D U deRegRequest into the specification. W h e n conditions are satisfied, the deRegRequest P D U is sent out and the F S M is transformed from a R E G I S T E R E D state to a I D L E state. This is not convenient for specification. 3. Expression: Sometimes the expressions are processed incorrectly. After changing the formula, the expressions can be computed correctly. For instance, changing not (a > b) into a < b enables T E S T G E N to run more smoothly.  Chapter 5.  Applying  Mobile IP to  TESTGEN  59  4. Single module: Because T E S T G E N can only process a single module, the test for the i n p u t / o u t p u t message from/to the module can not be done. In this thesis, we only assume that the home agent receives a RegRequest P D U , and sends out an Advertisement P D U , a RegReply P D U and a Datagram P D U . A n y tests on the communications between the home agent and mobile node can not be done. In the real test, it is necessary to test the communications among the home agent, the mobile node and the foreign agent. 5. Function of the subset: A t present, T E S T G E N can only support a very small subset of the Estelle language, which makes T E S T G E N tool very l i m i t e d , Hence, only a small protocol can be specified and fed into the T E S T G E N tool. In the real world, the protocols, such as the M o b i l e IP Protocol, are much bigger and more complex than that which can be specified i n Estelle.Y and A S N . l . It would be more practical i f T E S T G E N can support more features, such as communication between two entities, parallelism between two module instances, dynamic structure, more statements and variable types, and etc. 6. Constraints:  Some functions of constraints are duplicated.  For example, if the  m a x i m u m usage of R E G I S T E R E D state is increased, and the m a x i m u m usage of RegRequest and Datagram are not changed, no more test cases w i l l generated. Because only when some events, such as RegRequest and Datagram, happen, can the protocol state machine pass the state R E G I S T E R E D one more time. T h e usage of state and P D U / I S P are related.  Future study: 1. M o r e examples are needed to test every aspect of T E S T G E N to check if it works  Chapter 5. Applying  Mobile IP to  TESTGEN  60  perfectly according to its design. 2. T h e T E S T G E N tool can be expanded into several aspects: multiple modules, more data types, more statements and subroutines.  5.2  T h e Coverage O f T h e Test Suite T E S T G E N yields a large number of test cases, ranging from a few thousand to tens  of thousands.  These test cases are combinations of both the control sequences and  data variations. A l l of these test cases come from a few control sequences.  In these  control sequences, which have more coverage than the others? W h e n there are numerous control sequences, we must address this question. T h e T E S T S E L tool tries to answer this question. In this section, the algorithm of T E S T S E L is given, followed by the results of applying selection to the test suite i n the above section. T h e coverage w i l l be discussed in later section.  5.2.1  T h e algorithm of the test selection tool  A l l the test cases form a test space. In this space, some test cases are very close, i.e., the distance between them is short. However, some test cases are distant. If a set of test cases is to be selected, which w i l l be i n the final test case set? Figure 5.1 shows circle B is bigger than circle A , even there are both five test cases i n each circle. We would say test case set B has more coverage than test case set A , since the distance between B and the furthest test case to B is smaller than the distance between A and the furthest test case to A . B and A may have the same cost, since both B and A have five test cases and they may spend same steps to find these five test cases respectively. The formal algorithms of calculating the distance between test cases, the cost, and the  Chapter 5. Applying  Mobile IP to  \  TESTGEN  61  •• • • •  •  B  • test case space  • *  •  Figure 5.1: Test Case Space coverage are i n [ M V C 9 2 ] . T h e algorithm starts w i t h an empty set of the selected test cases T C , and the current cost (Cur_Cost) 0. W h i l e the tolerance (i.e., the distance between test cases) e is greater than e i m  n  for each test control sequence (tco) i n the test suite T S , the m i n i m u m distance  between tco and any test control sequence tc i n T S is calculated. If the m i n i m u m distance is greater than the current tolerance e , then the tco is added to the test cases T C . Once all the test control sequences i n the T S have been tested, the test selection tolerance e is shrunk by m u l t i p l i n g the user defined scale factor (Scale), and reiterating the algorithm until the m i n i m u m tolerance ( e i „ ) is reached or the m a x i m u m cost ( M a x C o s t ) is reached. m  T h e brief test selection algorithm is given as follows: 1. initialization: T C <— 0; Cur_Cost <— 0; 2. loop: while e > e  m t r i  {  reset T S ; while (there are unprocessed test cases i n T S ) {  Chapter 5. Applying  Mobile IP to  tc  TESTGEN  62  <— pick up a test case i n T S randomly;  0  distance  min xc  { l l dt(icn, tc) }; a  tce  if ( distance > e ) if ( Cur_Cost + Cost(rco) < M a x C o s t ) { T C <- T C U { tc  0  };  C u r . C o s t <— Cost(rco) + Cur_Cost ;  } else break from the inter while loop; M a r k the tco as processed  } e 4— e x Scale ;  }  where dt is a function to compute the distance between the two test control sequences and Cost is a function to compute the cost for the test control sequence.  A detailed  algorithm is i n [MVC92].  5.2.2  T h e results of the T E S T S E L  T h e results of running the T E S T S E L tool are given i n Table 5.1, including the information on test cases ( T C ) , control sequences ( C S ) , epsilon (Eps), m i n . epsilon (mJEps), max.  acceptable cost ( M C o s t ) , scale (Scale), real cost ( R C o s t ) , coverage (Coverage),  selected control sequence (SCS) and selected test cases ( S T C ) . X denotes no result i n this place.  Chapter 5. Applying  Mobile IP to  TESTGEN  63  Four groups of test selection results are given i n the table. In the first group there are 641 test cases generated by T E S T G E N .  These 641 test cases are composed from  4 test control sequences w i t h data variation. In the fourth group, there are 27802 test cases, which consist of 62 test control sequences w i t h data variation. F r o m Table 5.1, the following information can be observed, and some strong and weak points can be observed: • In the first group, if the parameter cost is set to be 20 and the scale to be 0.3, then the test selection finishes w i t h 5 real costs, 2 control sequences, 129 test cases and 76% for the test coverage. If the parameter cost is set to be 20, and the scale to be 0.1, then the test selection finishes w i t h 5 real costs, 1 control sequence, 128 test Group  1  2  3  4  TC  CS  Eps  m_Eps  MCost  Scale  641 641 641 641 641 641  4 4 4 4 4 4  529 529 529 529 529 17425 17425 17425 17425 17425 27802 27802 27802 27802  7 7 7 7 7  1.8 2.0 1.8 1.0 1.8 1.8 1.8 1.5 1.0 1.0 1.0 1.8 1.5 1.0 1.0 1.0 1.8 1.5 1.0 1.0  0.3 0.1 0.3 0.05 0.3 0.3 0.3 0.1 0.01 0.05 0.1 0.3 0.1 0.01 0.05 0.01 0.3 0.1 0.01 0.01  20 20 20 20 5 10 20 20 30 20 20 20 40 50 40 40 20 40 50 70  13 13 13 13 13 62 62 62 62  RCost  Coverage  SCS  STC  0.3 0.5 0.1 0.5 0.3 0.3 0.5 0.2 0.2 0.4 0.4  5 5 5 0 0 5 6 12 12 12 12  0.76 1.00 0.51 1.00 -49.0 0.76 0.88 0.88 1.00 1.00 0.94  2 4 1 4 0 2  0.5 0.2 0.5 0.3 0.1 0.5 0.2 0.5 0.5  6 12 12 24  0.88 0.88 0.99 0.98 1.00 0.75 0.88 0.94 0.99  129 296 128 296 0 129 257 257 521 521 265 X X X X X X X X X  36 16 33 48 37  3 3 7 7 5 3 3 9 7 13 5 7 24 39  Table 5.1: Results of the T E S T S E L for Specification i n E s t e l l e . Y + A S N . l  Chapter 5. Applying  Mobile IP to  TESTGEN  64  cases and 51% for the test coverage. If the epsilon and m i n . epsilon are changed as well, the test selection finishes w i t h 5 real cost, 4 control sequences, 296 test cases and the test coverage is 100%. • T h e strong points are: 1. T h e user can choose any parameter value to satisfy their requirement. If the bigger epsilon, smaller m i n . epsilon and smaller scale are chosen, then more control sequences are selected and more coverage is obtained. 2. It is an efficient tool for a big group of test cases, because the user can select more efficient test cases w i t h an acceptable cost and a satisfactory coverage from the whole collection of test cases. • T h e weak points are: 1. Real cost: T h e cost is the sum of the number of steps for selecting control sequences according to the parameters given by the user. — F r o m the data i n group one, we observed that almost a l l the test costs are 5, regardless of how many control sequences are selected and how much the coverage is. This is unrealistic i n the real world. It w i l l invariably cost more when more control sequences are selected and more coverage is obtained. — In another test case selection, we even have 4 control sequences selected w i t h no cost. — In one test case selection from the fourth group, 24 control sequences are selected w i t h the cost at 48 and the coverage at 94%. In another test case  Chapter 5. Applying  Mobile IP to  TESTGEN  65  selection w i t h the same parameters except w i t h the max. cost parameter at 70, 39 control sequences are selected w i t h cost at 37 and coverage at 99%.  This is unrealistic i n the real world.  F r o m the algorithm above,  the cost should be higher than 48 because 15 more control sequences are selected and 5% more coverage is reached. 2. Selection: In the selected control sequences, sometimes there are two similar control sequences, i.e., one control sequence is selected and put into the file twice. For example: Phase = 5, TC Id. = 0 (-Advertisement -, 1)  (RegRequest RegReply -, 1)  (- Advertisement -, 1)  (Datagram Datagram -, 1)  (DeRegRequest RegReply  1) (RegRequest RegReply -, 1)  Phase = 0, TC Id. = 0 (- Advertisement  1)  (- Advertisement -, 1)  (RegRequest RegReply -, 1) (Datagram Datagram  1)  (RegRequest RegReply -, 1) (DeRegRequest RegReply -, 1) In phase 0, test case 0 is selected and put into the file; In phase 5, test case 0 is selected and put into the file again. T h a t means one more control sequence and more duplicative test cases are collected later. F r o m the algorithm above, there should only be one test case 0 i n the test cases set to T C . 3. Coverage: W h e n 4 test control sequences are selected from 4 control sequences, the coverage is 100%. This is reasonable. W h e n no control sequence is selected,  Chapter 5.  Applying  Mobile IP to  TESTGEN  66  the coverage should be 0 instead of -49.00. T h e formula used w i t h no control sequence is 1 — 100.0/2.0 = —49.0. T h i s is incorrect. 4. Merging: F r o m 641 test cases, 4 control sequences are discovered. After merging these 4 control sequences w i t h data variation, there should be 641 test cases. Because the merge module reproduces the selected test cases i n the original form, i.e., all of the original instances generated by T E S T G E N should be included. B u t from the T E S T S E L , only 296 test cases are reproduced. We lose more than half the original test cases. T h e same happens i n the second group. 5. B i g group test cases: T E S T S E L is more useful for selecting- more efficient control sequences from a large number of control sequences generated from the T E S T G E N tool.. In the first group, the number of control sequences is 4, which is a bit small. Hence we have other groups w i t h more control sequences. T h e merging module does not work for the t h i r d and the fourth group. (The error report is " Wrong result i n i d J i l e and selectJile", but both id_file and selectJile are internal files i n the test selection tool.) So the complete selected test cases can not be obtained. T h i s defeats the function of T E S T S E L .  5.3  R e s u l t s f r o m the E s t e l l e . Z parser  T h e Estelle.Z specification language is defined, and its parser is implemented and linked w i t h the T E S T G E N kernel. To test whether the parser functions correctly w i t h the T E S T G E N kernel, the specifications of the home agent i n both Estelle.Z and Estelle. Y + A S N . l are fed into the T E S T G E N tool. If two exact test suites or two very similar test suites are generated by T E S T G E N , then the parser of Estelle.Z is working  Chapter  5.  Applying  Mobile IP to  67  TESTGEN  correctly. F r o m Figure 5.2, we can observe: i f we try to get exact or very similar test suites, then we need to have exact or very similar data structure the P D S for the same protocol specifications, because the T E S T G E N kernel generates test suites completely based on all information i n the P D S . A l l data i n the P D S are stored i n the internal file pds.file. There are two P D S files, the P D S l and the P D S 2 , for two home agent specifications, a specification i n E s t e l l e . Y + A S N . l and a specification i n Estelle.Z. After comparing the P D S l and the P D S 2 , we observed the P D S 2 is the same as the P D S l .  Besides, w i t h  the same constraints of the T E S T G E N tool, 641 test cases are generated for both home agent specifications. After fed into the T E S T S E L , two sets of 641 test cases result i n the same coverage and the same cost. The same results are developed for the three other groups. F r o m Table 5.2 and Table 5.1, we can conclude the the parser works well.  5.4  Summary  This chapter has discussed the algorithms of the T E S T G E N tool and the T E S T S E L tool, the two test suites from the T E S T G E N tool for home agent specification i n Est e l l e . Y + A S N . l and i n Estelle.Z, and the quality of the two test suites. The results of the T E S T S E L has demonstrated that the parser of Estelle.Z can be used to be the front part of the T E S T G E N tool, and the parser simplifies the protocol specifications. In addition, there is still further work to make the T E S T G E N + environment more practical and more efficient  Chapter 5.  Applying  Mobile IP to  TESTGEN  Figure 5.2: T w o Parsers  Chapter 5.  Group  1  2  3  4  Applying  TC 641 641 641 641 641 641 529 529' 529 529 529 17425 17425 17425 17425 17425 27802 27802 27802 27802  Mobile IP to  TESTGEN  69  CS  Eps  m_Eps  MCost  Scale  4 4 4 4 4 4  1.8 2.0 1.8 1.0 1.8 1.8 1.8 1.5 1.0 1.0 1.0  0.3 0.1 0.3 0.05 0.3 0.3 0-3 0.1 0.01 0.05 0.1  1.8 1.5 1.0 1.0 1.0 1.8 1.5 1.0 1.0  0.3 0.1 0.01 0.05 0.01 0.3 0.1 0.01 0.01  20 20 20 20 5 10 20 20 30 20 20 20 40 50 40 40 20 40 50 70  7 7 7 7 7 13 13 13 13 13 62 62 62 62  RCost  Coverage  SCS  STC  0.3 0.5 0.1 0.5 0.3 0.3 0.5 0.2 0.2 0.4 0.4  5 5 5 0 0 5 6 12 12 12 12  0.76 1.00 0.51 1.00 -49.0 0.76 0.88 0.88 1.00 1.00 0.94  2 4 1 4 0 2  0.5 0.2 0.5 0.3 0.1 0.5 0.2 0.5 0.5  6 12 12 24 36 16 33 48 37  0.88 0.88 0.99 0.98 1.00 0.75 0.88 0.94 0.99  129 296 128 296 0 129 257 257 521 521 265 X X X X X X X X X  3 3 7 7 5 3 3 9 7 13 5 7 24 39  Table 5.2: Results of the T E S T S E L for Specification i n Estelle.Z  Chapter 6  Conclusions and Future W o r k  6.1  Conclusions In this thesis, a front end has been developed for the protocol specification language,  Estelle.Z, which is based on Estelle I S O / I E C ISO 9074:1989(E). This front end performs the syntactic and semantic analysis of an Estelle.Z specification, and produces an annotated parse tree stored i n the P D S as the output.  It supports the m a i n structures  of the Estelle language. T h e new parser can accept the declarations of specifications i n Estelle.Z instead of i n A S N . l language, and can be easily expanded to complete Estelle language. A real world protocol, home agent - a component of M o b i l e IP, was used to test the parser.  First, the protocol was specified i n E s t e l l e . Y + A S N . l . T h r o u g h its parser, the  P D S was developed. A test suite was generated by the T E S T G E N tool, then the test suite was fed into the T E S T S E L tool, and a set of satisfactory test cases was developed. Also a set of constraints for T E S T G E N and a set of parameters for T E S T S E L were obtained. Second, the protocol was specified i n Estelle.Z. Through the Estelle.Z parser, the same P D S was developed as i n the E s t e l l e . Y + A S N . l parser.  A test suite was generated by  T E S T G E N , and the test suite was fed into T E S T S E L , the same set of selected test suite was successfully obtained, w i t h the same set of constraints for T E S T G E N and the same set of parameters for the T E S T S E L tool. B y comparing the two sets of data obtained  70  Chapter 6.  Conclusions and Future  Work  71  through the two parsers, we observed that the Estelle.Z parser works correctly. The framework established i n this thesis is quite powerful. T h e syntax of Estelle.Z can be expanded to the whole Estelle language easily. T h e tree structure is general and w i l l be augmented to support all of Estelle without any difficulty. To add more information in the tree structure, users simply augment the node structure. B y analyzing the results, T E S T G E N and T E S T S E L , the thesis discussed the advantage and l i m i t a t i o n of T E S T G E N and T E S T S E L .  6.2  Future W o r k  A number of features should be implemented or improved to enhance the function of the test suite generation environment T E S T G E N - | - listed as the following:  Parser The following needs to be done for the parser module i n the future: 1. A t present, the parser has been tested successfully by a real protocol specification, the home agent specification. Due to the time constraints, we only fed one real protocol specification to test the parser. It would be better to have had more real protocol specifications to test a l l aspects of the parser. 2. A number of features should be implemented to enhance the parser. Such as adding more data types, more statements, expanding the P D S to accommodate more information on the Estelle language, expanding the Estelle.Z to whole Estelle language to specify more complex real world protocols. This work needs to be done i n conjunction w i t h extension to the T E S T G E N engine.  Chapter 6.  Conclusions and Future  Work  72  3. Furthermore, the parser for S D L and L O T O S can be established to make the T E S T G E N + environment more widely used.  TESTGEN The following needs to be done for the T E S T G E N module i n the future: 1. E x p a n d the T E S T G E N engine to support multiple modules. In-the real world protocols, there are more than one module. For instance, i n M o b i l e IP, there are three modules: home agent, foreign agent and mobile host. To test the implementation of the whole mobile IP protocol, the test suite for the whole M o b i l e IP, including the home agent, the foreign agent and the mobile host, should be developed. In addition, w i t h only one module, it is impossible to test the cooperation among the modules. 2. E x p a n d the T E S T G E N engine to process more information i n the P D S . A s the parser processes the whole Estelle, the T E S T G E N engine should be able to process all the information i n the P D S to generate a test suite.  W i t h o u t the support  of the T E S T G E N engine, even i f the parser were expanded to whole Estelle, the T E S T G E N tool still does not make any more sense than before. Therefore, the parser and the T E S T G E N engine should be expanded at the same time. 3. Resolve the problems i n the T E S T G E N engine. T h e problems, such as the problems in the processing of assignment statements, need to be resolved. These problems prevent the T E S T G E N engine from generating meaningful test suites.  TESTSEL The following needs to be done for the T E S T S E L module i n the future: 1. Output. T h e selected test cases are i n an internal file. T h e y are neither i n subtours  Chapter 6.  Conclusions  and Future Work  .  73  which are readable by people, nor i n T T C N form which is standard test suite notation. It is necessary to modify the output into T T C N form to have T E S T S E L widely used. 2. Merging. Usually real protocols are huge, and the test cases are numerous, it is thus necessary to improve the merging module to process large test suites. 3. Cost. T h e cost is one of the indices to evaluate the quality of the selected test suite. F r o m m y practical experience on the home agent, the cost calculation does not correctly reflect the related cost for the test suite. Therefore it is necessary to improve this algorithm.  Bibliography  [Cho78]  T . S. Chow. Testing Software Design Modeled by F i n i t e State Machines . IEEE Transactions on Software Engineering, 4(3):178—187, M a r c h 1978.  [CVI89]  W . Y . L . C h a n , S. T . Vuong, and M . R . Ito. A n Improved Protocol Test Generation Procedure Based on U I O s . In Proc. of the ACM SIGCOMM '89, September 1989.  [Gon70]  G . Gonenc. A M e t h o d for the Design of Fault Detection Experiments. Transactions on Computers, 19(6) :551—558, June 1970.  [ISO]  ISO DIS/9646-3, OSI Conformance Testing Methodology and Framework, Part 3: The Tree and Tabular Combined Notation, march 1990. and interim working documents throughout 1990, particularly T T C N Extensions, I S O / I E C J T C 1/SC 21 N5077.  [LV93]  Sangho Lee and Son T . Vuong. T E S T G E N + : A n environment for protocol test suite generation, selection and validation, J u l y 1993.  IEEE  [MVC92] M . M c A l l i s t e r , S. T . Vuong, and J . Curgus. A u t o m a t e d Test Case Selection Based on Test Coverage Metrics. In Proc. of the IWPTS V, M o n t r e a l , Canada, September 1992. [Per96]  Charles Perkins. IP m o b i l i t y support, draft-ietf-mobileip-protocol-15.txt, Feb 1996.  [Pro92]  R . L . Probert. T T C N : the international notation for specifying tests of communications. Computer Networks and ISDN Systems, 23:417-438, 1992.  [SD88]  K . K . Sabnani and A . T . Dahbura. A Protocol Test Generation Procedure. Computer Networks and ISDN Systems, 15(4):285-297, September 1988.  [VCI89]  S. T . Vuong, W . Y . L . C h a n , and M . R . Ito. The U I O v - M e t h o d for Protocol Test Sequence Generation. In Proc. of the IWPTS II, B e r l i n , Germany, October 1989.  74  Appendix A  A S N . l specification of the simplified H o m e Agent in M o b i l e IP  HomeAgent  DEFINITIONS ::=  BEGIN  PduMessage ::= CHOICE { RegRequest, DeRegRequest, RegReply, Datagram, Datagrambak, Advertisement }  DeRegRequest ::= SEQUENCE { —  IP f i e l d s  ipSourceAddr  INTEGER,  —  addr. from which the msg i s sent  ipDestAddr  INTEGER,  —  addr. of f o r e i g n agent / home agent  75  Appendix  A. ASN.l  —  specification  of the simplified  Home Agent in Mobile IP  76  Mobile IP f i e l d s  mipType  INTEGER,  — set to 1  mipS  INTEGER,  — 1: simultaneous bindings"  mipHomeAddr  INTEGER,  — IP addr. of mobile node  mipHomeAgent  INTEGER, — IP addr. of mobile node's home agent  mipCOA  INTEGER,  mipldentification  INTEGER, — number constructed by mobile node  — IP addr of the end of the tunnel  — Mobile-Home Authentication Extension mipMHauthExtSPI  INTEGER,  Security Parameter Index (4 Bytes)  mipMHauthExtAuth  INTEGER  Authenticator, keyed MD5  ipSourceAddr  INTEGER,  addr. from which the msg i s sent  ipDestAddr  INTEGER,  addr. of f o r e i g n agent / home agent  }  RegRequest ::= SEQUENCE { — IP f i e l d s  --  Mobile IP f i e l d s  mipType  INTEGER,  set to 1  mipS  INTEGER,  1: simultaneous bindings  mipLifetime  INTEGER,  time remaining before expired  Appendix  A.  ASN.l  specification  of the simplified  Home Agent in Mobile IP  77  mipHomeAddr  INTEGER,  — IP addr. of mobile node  mipHomeAgent  INTEGER,  — IP addr. of mobile node's home agent  mipCOA  INTEGER,  — IP addr of the end of the tunnel  mipldentification  INTEGER,  — number constructed by  mobile node  — Mobile-Home Authentication Extension mipMHauthExtSPI  INTEGER,  — S e c u r i t y Parameter Index (4 Bytes)  mipMHauthExtAuth  INTEGER  - - Authenticator, keyed-MD5  ipSourceAddr  INTEGER,  — addr. from which the msg i s sent  ipDestAddr  INTEGER,  — addr. of foreign/home agent  }  RegReply  ::= SEQUENCE  { — IP f i e l d s  —  Mobile IP f i e l d s  mipType  INTEGER,  - - set to 3  mipCode  INTEGER,  - - the r e s u l t of r e g i s t r a t i o n request  mipLifetime  INTEGER,  -- time remaining before expired  mipHomeAddr  INTEGER,  -- IP addr. of mobile node  mipHomeAgent  INTEGER,  -- IP addr. of mobile node's home agent  mipldentification  INTEGER,  -- number constructed by  mobile node  Appendix  A. ASN.l  specification  of the simplified  Home Agent in Mobile IP  — Mobile-Home Authentication Extension mipMHauthExtSPI  INTEGER,  — Security Parameter Index- (4 Byt  mipMHauthExtAuth  INTEGER  — Authenticator, keyed MD5  }  Advertisement  ::= SEQUENCE  { — IP f i e l d s ipDestAddr  INTEGER,  m i l t i c a s e addr. or — l i m i t e d broadcase addr.  ipTTL  INTEGER,  IP f i e l d , must be set to 1  INTEGER,  - l i f e time of v a l i d advertisemt  — ICMP f i e l d s icmpLifetime  — i n t e r v a l = 1/3 icmpCode  INTEGER,  lifetime  — 0: as a router too  — M o b i l i t y Afent Advertisement Extension extRegLifetime  INTEGER,  — longest time acceptable f o r reg  extH  INTEGER (0..1)  — 1: t h i s i s a home agent  }  Datagram ::= SEQUENCE { ipDestAddr  INTEGER,  Appendix  A. ASN.l  specification  data  of the simplified  Home Agent in Mobile IP  INTEGER  }  Datagrambak : := SEQUENCE { ipDestAddr  INTEGER,  data  INTEGER  }  User ::= CHOICE { Junki }  Net  ::=  CHOICE  { Junko }  Junki ::= SEQUENCE { dummy  INTEGER  }  Junko ::= SEQUENCE { dummy  > END  INTEGER  Appendix B  E s t e l l e . Y specification of the simplified H o m e Agent in M o b i l e IP  s p e c i f i c a t i o n home_agent ;  CONST mipMHauthExtAuth  100 : i n t ;  mipMHauthExtSPI  200 : i n t ;  mipNodeHomeAddr  821012 : i n t ;  mipHomeAgent  821045 : i n t ;  mipS  1  localNetAddr  82832 : i n t ;  router  1  AdLifetime  : int;  : int;  = 18000 : i n t ;  RegLargestLifetime = 10 : i n t ;  VAR identification  int;  careOfAddr  int;  careOfAddrl  int;  bindno  int;  80  Appendix  B.  Estelle.Y  specification  of the simplified  ISP Junki  User;  Junko  Net;  OSP  PDU RegRequest DeRegRequest  recv_in  recv_in  Junki;  Junki;  RegReply  recv_in  Junki;  Datagram  recv_in  Junki;  Datagrambak  recv_in  Junki;  Advertisement  recv_in  Junki;  TIMER ad_timer  600;  STATE REGISTERED, IDLE ;  INITIALIZATION TO IDLE BEGIN bindno  := 0;  Home Agent in Mobile  IP  Appendix  B. Estelle.Y  specification  of the simplified  identification  := 0;  careOfAddr  := 0;  Home Agent in Mobile  END;  TRANS  FROM IDLE TO IDLE provided output  timeout(ad_timer)  Advertisement  begin Advertisement.ipDestAddr Advertisement.ipTTL  :=  := l o c a l N e t A d d r ; 1;  Advertisement.icmpLifetime Advertisement.icmpCode  :=  := A d L i f e t i m e ; 1;  Advertisement.extRegLifetime Advertisement.extH  :=  := R e g L a r g e s t L i f e t i m e ;  1;  end;  FROM IDLE TO REGISTERED when  RegRequest  provided (RegRequest.mipLifetime  > 0 )  IP  82  Appendix  B.  Estelle.Y  specification  of the simplified  Home Agent in Mobile  IP  AND (RegRequest.mipMHauthExtSPI  = mipMHauthExtSPI)  AND (RegRequest.mipMHauthExtAuth  = mipMHauthExtAuth)  AND (RegRequest.mipldentification > i d e n t i f i c a t i o n  )  AND (RegRequest.ipDestAddr output  = mipHomeAgent  )  RegReply  begin RegReply.ipSourceAddr  :=  RegReply.ipDestAddr  :=  RegReply.mipType  :=  mipHomeAgent; RegRequest.ipSourceAddr;  3;  RegReply.mipCode  := mipS;  RegReply.mipLifetime  := R e g R e q u e s t . m i p L i f e t i m e - 1 ;  RegReply.mipHomeAddr  :=  RegReply.mipHomeAgent  :=  „  RegRequest.mipHomeAddr; RegRequest.mipHomeAgent;  RegReply.mipldentification:=RegRequest.mipldentification+1 RegReply.mipMHauthExtSPI  :=RegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; identification if  (mipS = 0)  then begin  := R e g R e q u e s t . m i p l d e n t i f i c a t i o n +1  ;  Appendix  B. Estelle.Y  specification of the simplified Home Agent in Mobile IP  bindno := bindno + 1; if  (bindno = 1)  then  careOfAddr := RegRequest.mipCOA  else careOfAddr1 := RegRequest.mipCOA; end else begin careOfAddr := RegRequest.mipCOA; bindno := 1; end; end;  FROM IDLE TO IDLE when Datagram;  FROM IDLE TO IDLE when RegRequest provided RegRequest.ipDestAddr  = localNetAddr  output RegReply begin RegReply.ipSourceAddr := mipHomeAgent;  84  Appendix  B.  Estelle.Y  specification  of the simplified  Home Agent in Mobile  RegReply.ipDestAddr  := RegRequest.ipSourceAddr;  RegReply.mipType  := 3;  RegReply.mipLifetime  := RegRequest.mipLifetime-1;  RegReply.mipHomeAddr  :=  RegRequest.mipHomeAddr;  RegReply.mipHomeAgent  :=  RegRequest.mipHomeAgent;  IP  RegReply.mipldentification:=RegRequest.mipldentification+1 RegReply.mipCode  := 136;  RegReply.mipMHauthExtSPI  :=RegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; i d e n t i f i c a t i o n := RegRequest.mipldentification+1; end;  FROM REGISTERED TO IDLE when DeRegRequest provided (DeRegRequest.mipMHauthExtSPI = mipMHauthExtSPI AND (DeRegRequest.mipMHauthExtAuth = mipMHauthExtAuth) AND (DeRegRequest.ipDestAddr = mipHomeAgent )  output RegReply begin  Appendix  B.  Estelle.Y  specification of the simplified Home Agent in Mobile IP  RegReply.ipSourceAddr  :=  RegReply.ipDestAddr  :=  RegReply.mipType  := 3 ;  RegReply.mipCode  :=  0;  RegReply.mipLifetime  :=  0;  RegReply.mipHomeAddr  :=  DeRegRequest.mipHomeAddr;  RegReply.mipHomeAgent  :=  mipHomeAgent; DeRegRequest.ipSourceAddr;  DeRegRequest.mipHomeAgent;  RegReply.mipldentification:=DeRegRequest.mipldentification identification  :=  DeRegRequest.mipldentification;  RegReply.mipMHauthExtSPI  :=DeRegRequest.mipMHauthExtSPI;  bindno  := bindno -  1;  RegReply.mipMHauthExtAuth:=DeRegRequest.mipMHauthExtAuth;  if  (DeRegRequest.mipCOA = mipNodeHomeAddr)  then begin careOfAddr  :=  0;  careOfAddrl:=  0;  end else begin if  ( careOfAddr  then if  86  =DeRegRequest.mipCOA)  c a r e O f A d d r :=  0;  ( c a r e O f A d d r 1 =DeRegRequest.mipCOA  )  +1;  Appendix  B. Estelle. Y specification  then  of the simplified  careOfAddrl  :=  Home Agent in Mobile IP  0;  end; end;  FROM REGISTERED TO REGISTERED  provided timeout(ad_timer) output  Advertisement  begin Advertisement.ipDestAddr Advertisement.ipTTL  :=  := l o c a l N e t A d d r ; 1;  Advertisement.icmpLifetime Advertisement.icmpCode  :=  := A d L i f e t i m e ; 1;  Advertisement.extRegLifetime Advertisement.extH  :=  1;  end;  FROM REGISTERED TO REGISTERED  when Datagram p r o v i d e d ( b i n d n o <> 0 ) output  Datagram  := R e g L a r g e s t L i f e t i m e ;  87  Appendix  B.  Estelle.Y  specification  of the simplified  Home Agent in Mobile  begin Datagram.ipDestAddr Datagram.data  :=  :=  careOfAddr;  Datagram.data;  end;  FROM REGISTERED TO REGISTERED  when Datagram provided  ( bindno = 0 )  AND ( D a t a g r a m . i p D e s t A d d r = mipNodeHomeAddr) output  Datagram  begin if  ( router = 0 )  then begin Datagram.ipDestAddr Datagram.data  :=  :=  0;  0;  end else Datagram.ipDestAddr end;  FROM REGISTERED  := mipNodeHomeAddr;  IP  88  Appendix  B. Estelle.Y  specification of the simplified Home Agent in Mobile  TO REGISTERED  when Datagram provided  ( D a t a g r a m . i p D e s t A d d r = mipNodeHomeAddr ) AND  output  ( b i n d n o = 1)  Datagram  begin Datagram.ipDestAddr  := c a r e O f A d d r ;  end;  FROM REGISTERED TO REGISTERED  when Datagram provided  ( D a t a g r a m . i p D e s t A d d r = mipNodeHomeAddr ) AND ( b i n d n o = 2)  o u t p u t Datagram,  Datagrambak  begin Datagram.ipDestAddr  := c a r e O f A d d r ;  Datagrambak.ipDestAddr Datagrambak.data end;  FROM REGISTERED  :=  := c a r e O f A d d r l ;  Datagram.data;  IP  89  Appendix  B.  Estelle.Y  specification  of the simplified  Home Agent in Mobile  IP  TO REGISTERED  when RegRequest provided (RegRequest.mipMHauthExtSPI <>  mipMHauthExtSPI)  OR (RegRequest.mipMHauthExtAuth  <>  mipMHauthExtAuth)  output RegReply begin RegReply.ipSourceAddr := RegRequest.ipDestAddr; RegReply.ipDestAddr  := RegRequest.ipSourceAddr;  RegReply.mipType  := 3;  RegReply.mipCode  := 131;  RegReply.mipLifetime  := RegRequest.mipLifetime-1;  RegReply.mipHomeAddr  :=  RegRequest.mipHomeAddr;  RegReply.mipHomeAgent  :=  RegRequest.mipHomeAgent;  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI  := 0;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; i d e n t i f i c a t i o n := RegRequest.mipldentification+1; end;  FROM IDLE TO IDLE  Appendix  B. Estelle.Y  specification  of the simplified  Home Agent in Mobile IP  when RegRequest provided RegRequest.mipLifetime < 0 ;  FROM REGISTERED TO REGISTERED when RegRequest provided RegRequest.mipLifetime < 0 ;  FROM IDLE TO IDLE  when RegRequest provided (RegRequest.mipldentification < i d e n t i f i c a t i o n ) output RegReply begin RegReply.mipCode  := 133;  RegReply.mipLifetime  := RegRequest.mipLifetime-1;  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI  :=RegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; identification end;  := RegRequest.mipldentification+1;  Appendix  B.  Estelle.Y  specification  of the simplified  Home Agent in Mobile  FROM REGISTERED TO REGISTERED  when RegRequest provided (RegRequest.mipMHauthExtSPI = mipMHauthExtSPI) AND (RegRequest.mipMHauthExtAuth = mipMHauthExtAuth) AND (RegRequest.mipldentification > i d e n t i f i c a t i o n  )  AND (RegRequest.mipLifetime  > 0 )  AND ( mipS = 0 ) AND ( bindno = 1 ) output RegReply begin RegReply.ipSourceAddr  RegRequest.ipDestAddr;  RegReply.ipDestAddr  RegRequest.ipSourceAddr;  RegReply.mipType  3;  RegReply.mipCode  mipS;  RegReply.mipLifet ime  RegRequest.mipLifetime-1;  RegReply.mipHomeAddr  RegRequest.mipHomeAddr;  RegReply.mipHomeAgent  RegRequest.mipHomeAgent;  IP  Appendix  B.  Estelle.Y  specification  of the simplified  Home Agent in Mobile  IP  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI :=RegRequest.mipMHauthExtSPI; RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; identification  := RegRequest.mipldentification+1;  bindno := bindno + 1; careOfAddrl := RegRequest.mipCOA; end;  FROM REGISTERED TO REGISTERED  when RegRequest provided  (RegRequest.mipldentification < i d e n t i f i c a t i o n )  output beginRegReply RegReply.ipSourceAddr := RegRequest.ipDestAddr; RegReply.ipDestAddr  RegRequest.ipSourceAddr;  RegReply.mipType  3;  RegReply.mipCode  133;  RegReply.mipLifetime  RegRequest.mipLifetime-1;  RegReply.mipHomeAddr  RegRequest.mipHomeAddr;  RegReply.mipHomeAgent := RegRequest.mipHomeAgent;  Appendix  B.  Estelle.Y  specification  of the simplified  Home Agent in Mobile  IP  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI  :=RegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; i d e n t i f i c a t i o n := RegRequest.mipldentification+1; end;  FROM IDLE TO IDLE  when RegRequest provided not (RegRequest.mipMHauthExtSPI = mipMHauthExtSPI) OR not (RegRequest.mipMHauthExtAuth  = mipMHauthExtAuth)  output RegReply begin RegReply.ipSourceAddr  RegRequest.ipDestAddr;  RegReply.ipDestAddr  RegRequest.ipSourceAddr;  RegReply.mipType  3;  RegReply.mipCode  131;  RegReply.mipLifetime  RegRequest.mipLifetime-1;  RegReply.mipHomeAddr  RegRequest.mipHomeAddr;  RegReply.mipHomeAgent  RegRequest.mipHomeAgent;  RegReply.mipldentification:=RegRequest.mipldentification+1;  Appendix  B.  Estelle.Y  specification  of the simplified  RegReply.mipMHauthExtSPI  Home Agent in Mobile IP  := 0;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; identification end;  end.  := R e g R e q u e s t . m i p l d e n t i f i c a t i o n + 1 ;  95  Appendix C  Estelle.Z specification of the simplified H o m e Agent in M o b i l e IP  s p e c i f i c a t i o n home_agent ;  const mipMHauthExtAuth  = 100 ;  mipMHauthExtSPI  = 200 ;  mipNodeHomeAddr  = 821012;  mipHomeAgent  = 821045 ;  mipS  = i  localNetAddr  = 82832 ;  router  = i  AdLifetime  ;  ;  = 18000 ;  RegLargestLifetime = 10 ;  var  PduMessage : ( RegRequest, DeRegRequest, RegReply, Datagram, Datagrambak, Advertisement );  DeRegRequest :  96  Appendix  C. Estelle.Z  specification  of the simplified  Home Agent in Mobile  record ipSourceAddr  :  integer;  ipDestAddr  :  integer;  mipType  :  integer;  mipS  :  integer";  mipHomeAddr  :  integer;  mipHomeAgent  :  integer;  mipCOA  :  integer;  mipldentification :  integer;  mipMHauthExtSPI  :  integer;  mipMHauthExtAuth  :  integer;  end;  RegRequest : record ipSourceAddr  integer;  ipDestAddr  integer;  mipType  integer;  mipS  integer;  mipLifetime  integer;  mipHomeAddr  integer;  mipHomeAgent  integer;  mipCOA  integer;  mipldentification  integer;  IP  97  Appendix  C. Estelle.Z  specification  of the simplified  Home Agent in Mobile IP  mipMHauthExtSPI  :  integer;  mipMHauthExtAuth  :  integer;  ipSourceAddr  :  integer;  ipDestAddr  :  integer;  mipType  :  integer;  mipCode  :  integer;  mipLifetime  :  integer;  mipHomeAddr  :  integer;  mipHomeAgent  :  integer;  mipldentification :  integer;  mipMHauthExtSPI  :  integer;  mipMHauthExtAuth  :  integer;  end;  RegReply : record  end;  Advertisement : record ipDestAddr  integer;  ipTTL  integer ;  icmpLifetime  integer;  icmpCode  integer;  -  98  Appendix  C. Estelle.Z specification  of the simplified  Home Agent in Mobile IP  extRegLifetime  :  integer;  extH  :  integer;  ipDestAddr  :  integer;  data  :  integer;  ipDestAddr  :  integer;  data  :  integer;  :  integer;  end;  Datagram : record  end;  Datagrambak : record  end;  User : ( Junki );  Junki  : record dummy end;  Met : ( Junko );  99  Appendix  C. Estelle.Z specification  of the simplified  Home Agent in Mobile IP  Junko : record dummy end;  i d e n t i f i c a t i o n : integer; careOfAddr  : integer;  careOfAddrl  : integer;  bindno  : integer;  channel SPchannel(other, Net); by  other: Junki;  by  Net : Junko;  channel PDUchannel  ( pdu, other );  by pdu: RegRequest ; DeRegRequest ; RegReply ; Datagram ; Datagrambak ; Advertisement ;  :  integer;  Appendix  C. Estelle.Z  specification  of the simplified  Home Agent in Mobile  TIMER ad_timer  600;  state REGISTERED, IDLE ;  { i n i t i a l i z a t i o n part }  initialize  to  IDLE  begin bindno  := 0;  i d e n t i f i c a t i o n := 0; careOfAddr  := 0  end;  trans  FROM IDLE  { 1 }  TO IDLE  provided begin  timeout(ad_timer)  IP  Appendix  C. Estelle.Z specification  of the simplified  Advertisement.ipDestAddr Advertisement.ipTTL  :=  := l o c a l N e t A d d r ; 1;  Advertisement.icmpLifetime Advertisement.icmpCode  :=  := A d L i f e t i m e ; 1;  Advertisement.extRegLifetime Advertisement.extH output  :=  Home Agent in Mobile IP  := R e g L a r g e s t L i f e t i m e ;  1;  pdu.Advertisement;  end;  FROM IDLE  { 2 }  TO REGISTERED  when pdu.RegRequest provided (RegRequest.mipLifetime  > 0 )  and (RegRequest.mipMHauthExtSPI = mipMHauthExtSPI) and (RegRequest.mipMHauthExtAuth = mipMHauthExtAuth) and (RegRequest.mipldentification  > identification  and ( R e g R e q u e s t . i p D e s t A d d r = mipHomeAgent ) begin  f  )  Appendix  C. Estelle.Z specification  of the simplified Home Agent in Mobile IP  RegReply.ipSourceAddr  := mipHomeAgent;  RegReply.ipDestAddr  :=  RegReply.mipType  := 3;  RegReply.mipCode  := mipS;  RegReply.mipLifetime  :=  RegReply.mipHomeAddr  :=  RegReply.mipHomeAgent  :=  RegRequest.ipSourceAddr;  RegRequest.mipLifetime-1; RegRequest.mipHomeAddr; RegRequest.mipHomeAgent;  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI  :=RegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; identification if  := R e g R e q u e s t . m i p l d e n t i f i c a t i o n +1 ;  (mipS = 0)  then begin bindno if  := bindno  + 1;  (bindno = 1)  then  c a r e O f A d d r := RegRequest.mipCOA  else careOfAddr1  := RegRequest.mipCOA;  end else begin careOfAddr bindno end;  := RegRequest.mipCOA;  := 1;  103  Appendix  C. Estelle.Z specification  of the simplified  Home Agent in Mobile  IP  output pdu.RegReply; end;  FROM IDLE  { 3 }  TO IDLE when pdu.Datagram begin  end;  FROM IDLE  { 4  }  TO IDLE when pdu.RegRequest provided ( RegRequest.ipDestAddr = localNetAddr) begin RegReply.ipSourceAddr := mipHomeAgent; RegReply.ipDestAddr  := RegRequest.ipSourceAddr;  RegReply.mipType  := 3;  RegReply.mipLifetime  := RegRequest.mipLifetime-1;  RegReply.mipHomeAddr  :=  RegReply.mipHomeAgent  := RegRequest.mipHomeAgent;  RegRequest.mipHomeAddr;  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipCode  := 136;  RegReply.mipMHauthExtSPI  :=RegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth;  Appendix  C. Estelle.Z specification  identification output  :=  of the simplified  Home Agent in Mobile  IP  RegRequest.mipldentification+1;  pdu.RegReply;  end;  FROM REGISTERED  { 5 }  TO IDLE  when pdu.DeRegRequest provided (DeRegRequest.mipMHauthExtSPI = mipMHauthExtSPI) and (DeRegRequest.mipMHauthExtAuth = mipMHauthExtAuth) and ( D e R e g R e q u e s t . i p D e s t A d d r = mipHomeAgent ) begin RegReply.ipSourceAddr  := mipHomeAgent;  RegReply.ipDestAddr  := D e R e g R e q u e s t . i p S o u r c e A d d r ;  RegReply.mipType  := 3;  RegReply.mipCode  :=  0;  RegReply.mipLifetime  :=  0;  RegReply.mipHomeAddr  := DeRegRequest.mipHomeAddr;  R e g R e p l y . mipHomeAgent : = DeRegRequest. mipHomeAgent-; RegReply.mipldentification:=DeRegRequest.mipldentification identification  :=  DeRegRequest.mipldentification;  +1;  Appendix  C. Estelle.Z specification of the simplified Home Agent in Mobile  bindno  := bindno -  1;  RegReply.mipMHauthExtSPI  :=DeRegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=DeRegRequest.mipMHauthExtAuth; if  (DeRegRequest.mipCOA = mipNodeHomeAddr)  then begin careOfAddr  :=  0;  careOfAddrl:=  0;  end else begin if  ( c a r e O f A d d r = DeRegRequest.mipCOA)  then  c a r e O f A d d r := if  0;  ( c a r e O f A d d r l = DeRegRequest.mipCOA )  then  c a r e O f A d d r l :=  0;  end; output  pdu.RegReply;  end;  FROM REGISTERED TO REGISTERED  provided begin  timeout(ad_timer)  { 6 }  IP  Appendix  C. Estelle.Z specification  of the simplified  Advertisement.ipDestAddr Advertisement.ipTTL  :=  := l o c a l N e t A d d r ; 1;  Advertisement.icmpLifetime Advertisement.icmpCode  :=  := A d L i f e t i m e ; 1;  Advertisement.extRegLifetime Advertisement.extH output  :=  Home Agent in Mobile IP  := R e g L a r g e s t L i f e t i m e ;  1;  pdu.Advertisement;  end;  FROM REGISTERED  { 7 }  TO REGISTERED  when pdu.Datagram p r o v i d e d ( bindno <> 0 ) begin Datagram.ipDestAddr Datagram.data  :=  careOfAddr;  := D a t a g r a m . d a t a ;  output pdu.Datagram; end;  FROM REGISTERED TO REGISTERED  when pdu.Datagram  { 8 } .  Appendix  C. Estelle.Z specification  provided  of the simplified  Home Agent in Mobile  ( bindno = 0 )  AND ( D a t a g r a m . i p D e s t A d d r = mipNodeHomeAddr) • begin if  ( router = 0 )  then begin Datagram.ipDestAddr Datagram.data  :=  :=  0;  0;  end else Datagram.ipDestAddr output  := mipNodeHomeAddr;  pdu.Datagram;  end;  FROM REGISTERED  { 9 }  TO REGISTERED  when pdu.Datagram provided  ( D a t a g r a m . i p D e s t A d d r = mipNodeHomeAddr ) AND  ( b i n d n o = 1)  begin Datagram.ipDestAddr output end;  pdu.Datagram;  := c a r e O f A d d r ;  IP  Appendix  C. Estelle.Z specification of the simplified Home Agent in Mobile  FROM REGISTERED  { 10  }  TO REGISTERED  when pdu.Datagram provided  ( D a t a g r a m . i p D e s t A d d r = mipNodeHomeAddr ) AND ( bindno = 2)  begin Datagram.ipDestAddr  := c a r e O f A d d r ;  Datagrambak.ipDestAddr Datagrambak.data output output  :=  := c a r e O f A d d r l ;  Datagram.data;  pdu.Datagram;  pdu.Datagrambak;  end;  FROM REGISTERED  { 11  }  TO REGISTERED  when  pdu.RegRequest  provided (RegRequest.mipMHauthExtSPI  <> mipMHauthExtSPI)  OR (RegRequest.mipMHauthExtAuth begin  <>  mipMHauthExtAuth)  IP  Appendix  C. Estelle.Z specification  of the simplified  Home Agent in Mobile  IP  RegReply.ipSourceAddr := RegRequest.ipDestAddr RegReply.ipDestAddr  := RegRequest.ipSourceAddr;  RegReply.mipType  := 3;  RegReply.mipCode  := 131;  RegReply.mipLifetime  := RegRequest.mipLifetime-1;  RegReply.mipHomeAddr  := RegRequest.mipHomeAddr;  RegReply.mipHomeAgent  := RegRequest.mipHomeAgent;  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI := 0; RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; i d e n t i f i c a t i o n := RegRequest.mipldentification+1; output pdu.RegReply; end;  FROM IDLE  { 12 }  TO IDLE when pdu.RegRequest provided RegRequest.mipLifetime < 0 begin  end;  FROM REGISTERED TO REGISTERED when pdu.RegRequest provided RegRequest.mipLifetime < 0  { 13 }  Appendix  C. Estelle.Z specification  begin  of the simplified  Home Agent in Mobile  IP  end;  FROM IDLE  { 14 }  TO IDLE  when pdu.RegRequest provided (RegRequest.mipldentification < i d e n t i f i c a t i o n ) begin RegReply.mipCode  := 133333;  RegReply.mipLifetime  := RegRequest.mipLifetime-1;  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI  :=RegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; identification  := RegRequest.mipldentification+1;  output pdu.RegReply; end;  FROM REGISTERED  { 15 }  TO REGISTERED  when pdu.RegRequest provided (RegRequest.mipMHauthExtSPI = mipMHauthExtSPI)  Appendix  C. Estelle.Z specification  of the simplified  Home Agent in Mobile IP  AND (RegRequest.mipMHauthExtAuth  = mipMHauthExtAuth)  AND (RegRequest.mipldentification > i d e n t i f i c a t i o n  )  AND (RegRequest.mipLifetime > 0 ) AND ( mipS = 0 ) AND ( bindno  = 1 )  begin R e g R e p l y . i p S o u r c e A d d r ':=  RegRequest.ipDestAddr;  RegReply.ipDestAddr  :=  RegRequest.ipSourceAddr;  RegReply.mipType  :=  RegReply.mipCode  := mipS;  R e g R e p l y . m i p L i f e t ime  :=  RegReply.mipHomeAddr  :=  RegRequest.mipHomeAddr;  RegReply.mipHomeAgent  :=  RegRequest.mipHomeAgent;  3;  RegRequest.mipLifetime-1;  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI  :=RegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; identification bindno  :=  := bindno  careOfAddrl  :=  RegRequest.mipldentification+1; +1;  RegRequest.mipCOA;  output pdu.RegReply '  112  Appendix  C. Estelle.Z specification  of the simplified  Home Agent in Mobile  IP  end;  FROM REGISTERED  { 16 }  TO REGISTERED  when pdu.RegRequest provided (RegRequest.mipldentification < i d e n t i f i c a t i o n ) begin RegReply.ipSourceAddr := RegRequest.ipDestAddr; RegReply.ipDestAddr  := RegRequest.ipSourceAddr;  RegReply.mipType  := 3;  RegReply.mipCode  := 133;  RegReply.mipLifetime  := RegRequest.mipLifetime-1;  RegReply.mipHomeAddr  :=  RegReply.mipHomeAgent  := RegRequest.mipHomeAgent;  RegRequest.mipHomeAddr;  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI  :=RegRequest.mipMHauthExtSPI;  RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; identification  := RegRequest.mipldentification+1;  output pdu.RegReply; end;  FROM IDLE  { 17 }  Appendix  C. Estelle.Z specification  of the simplified  Home Agent in Mobile  IP  TO IDLE  when pdu.RegRequest provided not  (RegRequest.mipMHauthExtSPI = mipMHauthExtSPI)  or not  (RegRequest.mipMHauthExtAuth  = mipMHauthExtAuth)  begin RegReply.ipSourceAddr := RegRequest.ipDestAddr; RegReply.ipDestAddr  := RegRequest.ipSourceAddr;  RegReply.mipType  := 3;  RegReply.mipCode  := 131;  RegReply.mipLifetime  := RegRequest.mipLifetime-1;  RegReply.mipHomeAddr  :=  RegRequest.mipHomeAddr;  RegReply.mipHomeAgent  :=  RegRequest.mipHomeAgent;  RegReply.mipldentification:=RegRequest.mipldentification+1; RegReply.mipMHauthExtSPI := 0; RegReply.mipMHauthExtAuth:=RegRequest.mipMHauthExtAuth; i d e n t i f i c a t i o n := RegRequest.mipldentification+1; output pdu.RegReply; end; end.  Appendix D  A S N . l specification of message parameters for the complete H o m e Agent  Home Agent processes five types of messages: Registration Request, DeRegistration Request, Registration Reply, Advertisement and datagram. We specify these messages i n A S N . l to describe their whole parameters.  HomeAgent  DEFINITIONS ::=  BEGIN  PduMessage ::= CHOICE { RegRequest, DeRegRequest, RegReply, Datagram, Advertisement }  RegRequest ::= SEQUENCE  115  Appendix  D. ASN.l  specification  of message parameters for the complete Home  AgentllQ  { — IP f i e l d s  ipSourceAddr  INTEGER,  —  addr. from which the msg i s sent  ipDestAddr  INTEGER,  —  addr. of foreign/home agent  — UDP f i e l d s  udpSourcePort  INTEGER,  —  variable  udpDestPort  INTEGER,  —  constant 434  Mobile IP  fields  mipType  INTEGER,  —  set to 1 ( r e g i s t r a t i o n request)  mipS  INTEGER,  —  1: simultaneous bindings  mipB  INTEGER,  —  1: broadcase datagrams required  mipD  INTEGER,  —  1: decapsulation by mobile node  mipM  INTEGER,  —  1: minimal encapsulation  mipG  INTEGER,  —  1: GRE encapsulation.  mipV  INTEGER,  —  1: Van Jacobson header compression  mipRSV  INTEGER,  —  reserved b i t s ,  mipLifetime  INTEGER,  —  time remaining before expired  mipHomeAddr  INTEGER,  —  IP addr. of mobile node  mipHomeAgent  INTEGER, —IP  sent as 0  addr. of mobile node's home agent  Appendix  D. ASN. 1 specification  mipCOA  of message parameters for the complete Home Agentl 17  INTEGER,  —  IP addr of the end of the tunnel  m i p l d e n t i f i c a t i o n INTEGER,—number constructed by the mobile node  —  Mobile-Home Authentication Extension  mipMHauthExtType  INTEGER,  -- 32  mipMHauthExtLength  INTEGER,  —  mipMHauthExtSPI  INTEGER,  -- Security Parameter Index (4 Bytes)  mipMHauthExtAuth  INTEGER,  -- Authenticator, keyed MD5  —  4 + length of authenticator  Mobile-Foreign Authentication Extension,  optional  mipMFauthExtType  INTEGER,  --33  mipMFauthExtLength  INTEGER,  —  4 + length of authenticator  mipMFauthExtSPI  INTEGER,  —  S e c u r i t y Parameter Index (4 Bytes)  mipMFauthExtauth  INTEGER,  —  authenticator, keyed MD5  —  Foreign-Home Authentication Extension,  optional  mipFHauthExtType  INTEGER,  —  34  mipFHauthExtLength  INTEGER,  —  4 + length of authenticator  mipFHauthExtSPI  INTEGER,  —  S e c u r i t y Parameter Index (4 Bytes)  mipFHauthExtAuth  INTEGER  —  Authenticator, keyed MD5  }  Appendix  D. ASN. 1 specification  DeRegRequest  of message parameters for the complete Home Agent!  ::= SEQUENCE  { —  IP  fields  ipSourceAddr  INTEGER,  -  a d d r . from which t h e msg- i s  ipDestAddr  INTEGER,  -  addr.  ~  of foreign/home  agent  UDP f i e l d s  udpSourcePort  INTEGER,  -  variable  udpDestPort  INTEGER,  -  constant  —  sent  M o b i l e IP  434  fields  mipType  INTEGER,  -  set  mipS  INTEGER,  -  1:  mipB  INTEGER,  -  1: b r o a d c a s e datagrams r e q u i r e d  mipD  INTEGER,  -  1: d e c a p s u l a t i o n by m o b i l e node  mipM  INTEGER,  -  1: m i n i m a l  mipG  INTEGER,  -  1: GRE e n c a p s u l a t i o n  mipV  INTEGER,  -  1: Van J a c o b s o n h e a d e r  mipRSV  INTEGER,  -  reserved b i t s ,  to  1 (registration  simultaneous  request)  bindings  encapsulation  compression  sent as 0  Appendix  D. ASN. 1 specification  of message parameters for the complete Home Agent! 19  mipHomeAddr  INTEGER,  —  IP addr. of mobile node  mipHomeAgent  INTEGER, — I P addr. of mobile node's home agent  mipCOA  INTEGER,  -- IP addr of the end of the tunnel  m i p l d e n t i f i c a t i o n INTEGER,—number constructed by the mobile node  —  Mobile-Home Authentication Extension  mipMHauthExtType  INTEGER,  -- 32  mipMHauthExtLength  INTEGER,  —  4 + length of authenticator  mipMHauthExtSPI  INTEGER,  —  S e c u r i t y Parameter Index (4 Bytes)  mipMHauthExtAuth  INTEGER,  —  Authenticator, keyed MD5  —  Mobile-Foreign Authentication Extension,  optional  mipMFauthExtType  INTEGER,  —  33  mipMFauthExtLength  INTEGER,  —  4 + length of authenticator  mipMFauthExtSPI  INTEGER,  —  S e c u r i t y Parameter Index (4 Bytes)  mipMFauthExtauth  INTEGER,  —  authenticator, keyed MD5  —  Foreign-Home Authentication Extension,  optional  mipFHauthExtType  INTEGER,  —  34  mipFHauthExtLength  INTEGER,  —  4 + length of authenticator  mipFHauthExtSPI  INTEGER,  —  S e c u r i t y Parameter Index (4 Bytes)  Appendix  D. ASN. 1 specification  mipFHauthExtAuth  of message parameters  for the complete Home  INTEGER  - - A u t h e n t i c a t o r , keyed MD5  ipSourceAddr  INTEGER,  - - a d d r . from which t h e msg i s  ipDestAddr  INTEGER,  ~  udpSourcePort  INTEGER,  — variable  udpDestPort  INTEGER,  - - constant  Agentl20  }  RegReply  ::= SEQUENCE  { —  ~  —  mipType  IP f i e l d s  addr.  sent  o f f o r e i g n / h o m e agent  UDP f i e l d s  434  M o b i l e IP f i e l d s  INTEGER,  — set  to 3 ( r e g i s t r a t i o n request)  endix D. ASN.l  specification  of message parameters  for the complete Home  Agentl21  mipCode  INTEGER,  —  the r e s u l t of r e g i s t r a t i o n request  mipLifetime  INTEGER,  —  time remaining before expired  mipHomeAddr  INTEGER,  —  IP addr. of mobile node  mipHomeAgent  INTEGER, —  mipldentification  INTEGER, —number constructed by the mobile node  —  IP addr. of mobile node's home agent  Mobile-Home Authentication Extension  mipMHauthExtType  INTEGER,  -- 32  mipMHauthExtLength  INTEGER,  —  mipMHauthExtSPI  INTEGER,  - - S e c u r i t y Parameter Index (4 Bytes)  mipMHauthExtAuth  INTEGER,  —  —  4 + length of authenticator  Authenticator, keyed MD5  Mobile-Foreign Authentication Extension,  optional  mipMFauthExtType  INTEGER,  -- 33  mipMFauthExtLength  INTEGER,  -- 4 + length of authenticator  mipMFauthExtSPI  INTEGER,  —  mipMFauthExtauth  INTEGER,  -- authenticator, keyed MD5  —  S e c u r i t y Parameter Index (4 Bytes)  Foreign-Home Authentication Extension,  optional  mipFHauthExtType  INTEGER,  —  34  mipFHauthExtLength  INTEGER,  —  4 + length of authenticator  Appendix  D. ASN. 1 specification  of message parameters  for the complete Home  mipFHauthExtSPI  INTEGER,  ~  mipFHauthExtAuth  INTEGER  -- Authenticator, keyed MD5  Agentl22  S e c u r i t y Parameter Index (4 Bytes)  }  Advertisement ::= SEQUENCE {  —  Link-Layer f i e l d s - l i n k l a y e r dest. addr.  linkDestAddr  —  INTEGER,  IP f i e l d s  ipTTL  INTEGER,  ipDestAddr  INTEGER,  IP f i e l d , must be set to 1 - m i l t i c a s e addr. or —  —  l i m i t e d broadcase addr.  ICMP f i e l d s  icmpCode  INTEGER,  —  0: as a router too —  icmpLifetime  INTEGER,  —  l i f e time of v a l i d —  icmpRouterAddr  INTEGER,  icmpNumAddrs  INTEGER,  —  i : not handle common t r a f f i c advertisemt  i n t e r v a l = 1/3 l i f e t i m e  may be set to 0  Appendix  D. ASN. 1 specification  —  of message parameters  for the complete Home  Agentl23  M o b i l i t y Afent Advertisement Extension  extType  INTEGER,  — 16  extLength  INTEGER,  -- 6 + 4 * N —  N = No. Of Care of Addresses  extSeqNum  INTEGER,  —  0 .. O x f f f f - 256  extRegLifetime  INTEGER,  —  longest time acceptable  extR  INTEGER,  — 1: f o r FA, Reg. required  extB  INTEGER,  — 1: busy  extH  INTEGER, —  extF  INTEGER,  — 1: t h i s i s a f o r e i g n agent  extM  INTEGER,  — 1: minimal encapsulation  extG  INTEGER,  — 1: GRE encapsulation  extV  INTEGER,  —  l:Van Jacobson header compression  extReserved  INTEGER,  —  reserved, 0  extCOA  INTEGER  —  f o r f o r e i g n agent, Care Of Addr.  —  1: t h i s i s a home agent  Prefix-Lengths Extension, optional  PLextType  INTEGER,  — 19  PLextLength  INTEGER,  —  length  PLextPrelen  INTEGER,  —  P r e f i x Length(s)  Appendix  D. ASN. 1 specification  —  of message parameters for the complete Home  One-byte Padding E x t e n s i o n ,  OBType  INTEGER  optional  — 0  }  Datagram ::= {  SEQUENCE — there —  } END  not datagram format i n t h i s  here only n e c e s s a r y / r e l a t e d  ipDestAddr data  is  INTEGER, ' INTEGER  fields  document are  declared  Agentl24  Appendix E  Selected C o n t r o l Sequences and Test Cases  There are 529 test cases generated by T E S T G E N , i n which there are 7 control sequences. We feed the 7 control sequences into T E S T S E L , then we got 5 control sequences w i t h the coverage 94.5% and the cost 12. T h e 7 control sequences and the 5 control sequences are as the follows: 1. Advertisement  -  RegRequest  Datagram Datagram -  RegReply  -  RegRequest RegReply -  -  Advertisement  DeRegRequest RegReply  -  2. RegRequest  RegReply  -  RegRequest RegReply -  -  Advertisement  DeRegRequest  -  Datagram  RegReply  -  -  Datagram  -  Advertisement  -  3. RegRequest Datagram  RegReply Datagram  -  -  Advertisement  DeRegRequest  -  RegRequest  RegReply  -  -  RegReply  -  Advertisement  -  4 RegRequest  RegReply  RegRequest  RegReply -  -  Datagram  Datagram  DeRegRequest  -  -  Advertisement  RegReply  -  -  -  Advertisement  -  5. RegRequest -  RegReply  Advertisement  -  - Datagram DeRegRequest  Datagram RegReply  125  -  RegRequest -  -  RegReply  Advertisement  -  Appendix  E. Selected Control Sequences and Test Cases  126  6. RegRequest Datagram  RegReply Datagram  -  RegRequest  RegReply  -  -  Advertisement  -  DeRegRequest  RegReply  -  -  Advertisement  -  7.  RegRequest  RegReply  Advertisement  -  -  RegRequest RegReply  DeRegRequest  RegReply  - Datagram -  -  Datagram  -  Advertisement  T h e parameters used i n T E S T S E L are: Eps = 1.000000, M i n J E p s = 0.100000, Scale = 0.4, M a x C o s t = 20 T h e selected control sequences are:  Phase = 0, TC Id. = 0 (- Advertisement  1)(RegRequest RegReply -, 1 ) ( - Advertisement  (Datagram Datagram -, 1)  (RegRequest RegReply  1)  (DeRegRequest RegReply -, 1)  Phase = 1, TC Id. = 2 (RegRequest RegReply -, 1 ) ( - Advertisement -, 1) (RegRequest RegReply -, 1)  (Datagram Datagram -, 1)  (DeRegRequest RegReply -, 1 ) ( - Advertisement -, 1)  Phase = 1, TC Id. = 36 (RegRequest RegReply -, 2) (- Advertisement -, 1)  (Datagram Datagram  1)  (DeRegRequest RegReply -, 1)  1)  Appendix  E. Selected Control Sequences and Test Cases  (- Advertisement -, 1)  Phase = 2, TC Id. = 1 (RegRequest RegReply -, 1) (Datagram Datagram  1)  (- Advertisement  1)  (RegRequest RegReply -, 1)  (DeRegRequest RegReply -, 1 ) ( - Advertisement  1)  Phase = 2, TC Id. = 19 (RegRequest RegReply -, 1)(Datagram Datagram -, 1) (RegRequest RegReply -, 1) (- Advertisement -, 1) (DeRegRequest RegReply -, 1)  (- Advertisement -, 1)  Coverage = 0.945312 with Cost : 12  Appendix  **  E. Selected Control Sequences and Test Cases  128  0  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / Datagram 1 1 - - - - /  Datagram 821020 1  _ / _ _ _ _ _ _ _  RegRequest 8285 82832 1 1 10 821012 821045 821020 5 200 100 / RegReply 82832 99 3 131 98 99 99 21 0 150 / DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  **  1  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 82832 1 1 10 821012 821045 821020 5 200 100 / RegReply 82832 99 3 131 98 99 99 21 0 150 / Datagram 1 1 - - - - /  Datagram 821020 1  _ _ / _ _  - - -  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200. 100-/ RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  Appendix  **  E. Selected Control Sequences and Test Cases  129  2  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 82832 1 1 10 821012 821045 821020 5 200 150 / RegReply 82832 99 3 131 98 99 99 21 0 150 / Datagram 1 1 - - - - /  Datagram 821020 \ - - - - / - - - - -  - -  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  **  3  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 82832 1 1 10 821012 821045 821020 5 250 100 / RegReply 82832 99 3 131 98 99 99 21 0 150 / Datagram 1 1 - -  / Datagram 821020 1  - - / - - - - - - -  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 /  Appendix  E. Selected Control Sequences and Test Cases  130  /Advertisement 82832 1 18000 1 1 0 1 /  **  4  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 82832 1 1 10 821012 821045 821020 5 250 150 / RegReply 82832 99 3 131 98 99 99 21 0 150 / Datagram 1 1 -  / Datagram 821020  1 - - - - / - - - - - . - -  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  **  5  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 82832 1 1 10 821012 821045 821020 20 200 100 / RegReply 82832 99 3 131 98 99 99 21 0 150 / Datagram 1 1 - -  / Datagram 821020  l - - - - / - - - - - - -  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 /  Appendix  E. Selected Control Sequences and Test Cases  131  /Advertisement 82832 1 18000 1 1 0 1 /  **  6  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 82832 1 1 10 821012 821045 821020 20 200 150 / RegReply 82832 99 3 131 98 99 99 21 0 150 / Datagram 1 1  .- / Datagram 821020 1 -  - /  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  **  7  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 82832 1 1 10 821012 821045 821020 20 250 100 / RegReply 82832 99 3 131 98 99 99 21 0 150 / Datagram 1 1  / Datagram 821020 1  /  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 /  Appendix  E. Selected Control Sequences and Test Cases  132  /Advertisement 82832 1 18000 1 1 0 1 /  **  8  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 82832 1 1 10 821012 821045 821020 20 250 150 / RegReply 82832 99 3 131 98 99 99 21 0 150 / Datagram 1 1 - - - - /  Datagram 821020 1 - - - - / - - - -  -  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  **  9  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  °- -  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 133 9 821012 821045 6 200 100./ Datagram 1 1 - - - - /  Datagram 821020 \ - - - - / - - - - -  - -  Appendix  E. Selected Control Sequences and Test Cases  133  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply -  821045 821012 3 0 0 821012 821045 51 200 100 /  "  /Advertisement 82832 1 18000 1 1 0 1 /  **  10  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 150 / RegReply 821045 8285 3 133 9 821012 821045 6'200 1 0 0 / Datagram 1 1 - - - - /  Datagram 821020 1  _ _ / - _ _ _ _ _ _  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  **  11  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 821045 1 1 10 821012 821045 821020 5 250 100 / RegReply 821045 8285 3 133 9 821012 821045 6 200 100 / Datagram 1 1 - - - - /  Datagram 821020 1 - - - - /  _ _ _ _ _  Appendix  E. Selected Control Sequences and Test Cases  134  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  **  12  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 821045 1 1 10 821012 821045 821020 5 250 150 / RegReply 821045 8285 3 133 9 821012 821045 6 200 100 / Datagram 1 1 - - - - /  Datagram 821020  1 - - - - / - - - - - - -  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / -  **  13  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 821045 1 1 10 821012 821045 821020 20 200 100 / RegReply 821045 8285 3 133 9 821012 821045 6 200 100 / Datagram 1 1  / Datagram 821020 1  - / -  -  Appendix  E. Selected Control Sequences and Test Cases  DeRegRequest  135  821012 821045 1 1 821012 821045 0 50 200 100 /  RegReply  821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement  **  82832 1 18000 1 1 0  1/  14  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / 821045 8285 3 1 9  RegReply  821012 821045 6 200 100 /  /Advertisement  82832 1 18000 1 1 0  1/  RegRequest 8285 821045 1 1 10 821012 821045 821020 20 200 150 / 821045 8285 3 133 9 821012 821045 6 "200 100 / Datagram 1 1 DeRegRequest  RegReply  •-  / Datagram 821020 1  /  -  821012 821045 1 1 821012 821045 0 50 200 100 /  RegReply  821045 821012 3 0 0 821012 821045 51 200 1 0 0 / /Advertisement  **  82832 1 18000 1 1 0  1/  15  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / 821045 8285 3 1 9  RegReply  821012 821045 6 200 100 /  /Advertisement  82832 1 18000 1 1 0  1/  RegRequest 8285 821045 1 1 10 821012 821045 821020 20 250 100 /  RegReply  821045 8285 3 133 9 821012 821045 6 200 100 / Datagram 1 1  - - / Datagram 821020 1 - - - - /  - -  -  Appendix  E. Selected Control Sequences and Test Cases  136  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 /  **  16  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / RegRequest 8285 821045 1 1 10 821012 821045 821020 20 250 150 / RegReply 821045 8285 3 133 9 821012 821045 6 200 100 / Datagram 1 1 - - - - / Datagram 821020 l  - ' - - ' - / - - - - - - -  DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / /Advertisement 82832 1 18000 1 1 0 1 / **  17  RegRequest 8285 821045 1 1 10 821012 821045 821020 5 200 100 / RegReply 821045 8285 3 1 9 821012 821045 6 200 100 / RegRequest 8285 82832 1 1 10 821012 821045 821020 5 200 100 / RegReply 82832 99 3 131 98 99 99 21 0 150 / Datagram 1 1  / Datagram 821020 1  /  /Advertisement 82832 1 18000 1 1 0 1 / DeRegRequest 821012 821045 1 1 821012 821045 0 50 200 100 / RegReply 821045 821012 3 0 0 821012 821045 51 200 100 / _  /Advertisement 82832 1 18000 1 1 0 1 /  Appendix F  4 T y p i c a l Control Sequences and T y p i c a l test cases in T T C N . M P  1. Datagram - - RegRequest  2.  RegReply - - A d v e r t i s e m e n t  RegRequest  RegReply - DeRegRequest  RegRequest  RegReply - - A d v e r t i s e m e n t  DeRegRequest RegReply - RegRequest 3.  RegRequest  4. RegRequest  -  -  RegRequest  DeRegRequest  RegReply -  i n TTCN.MP:  suiteOOOl  $DeclarationsPart $Begin_TS_ConstDcls $TS_ConstDcl $TS_ConstId  mipMHauthExtAuth  $TS_ConstType $TS_ConstValue  RegReply  RegReply  $Suite $SuiteId  - Datagram Datagram -  - DeRegRequest RegReply - RegRequest  RegReply  Advertisement  T e s t Cases  RegReply -  RegReply - Datagram Datagram -  Advertisement  INTEGER 100  $End_TS_ConstDcl  137  -  -  RegReply -  Datagram  -  -  Appendix  F. 4 Typical Control Sequences and Typical test cases in TTCN.MP  $TS_ConstDcl $TS_ConstId  mipMHauthExtSPI  $TS_ConstType  INTEGER  $TS_ConstValue  200  $End_TS_ConstDcl  $Begin_ASNl_PDU_TypeDef $PDU_Id  DeRegRequest  $PC0_TypeId $Comment $ASNl_TypeDefinition SEQUENCE { ipSourceAddr ipDestAddr mipType mipS  INTEGER,  INTEGER,  INTEGER,  mipHomeAddr mipHomeAgent mipCOA  INTEGER,  INTEGER, INTEGER,  INTEGER,  mipldentification mipMHauthExtSPI mipMHauthExtAuth >  INTEGER, INTEGER, INTEGER  138  Appendix  F. 4 Typical  Control Sequences and Typical test cases in TTCN.MP  $End_ASNl_TypeDefinition $End_ASNl_PDU_TypeDef  $Begin_ASNl_PDU_Constraint $ConsId  RegRequest_62  $PDU_Id  RegRequest  $DerivPath $ASNl_ConsValue { ipSourceAddr ipDestAddr mipType mipS  8285 , 821045 ,  1, 1,  mipLifetime  10 ,  mipHomeAddr  821012 ,  mipHomeAgent mipCOA  821045 ,  821020 ,  mipldentification mipMHauthExtSPI mipMHauthExtAuth  5 , 200 , 100  >  $End_ASNl_PDU_Constraint  $Begin_TestCase  139  Appendix  F. 4 Typical  Control Sequences and Typical  $TestCaseId test30 $TestPurpose test_test30 $BehaviourDescription $End_BehaviourDescription $BehaviourLine $Label $Line [4] ! RegReply $Cref  RegReply_215  $Verdict $Comment { ipSourceAddr ipDestAddr  821045 , 821012 ,  mipType  3 ,  mipCode  0 ,  mipLifetime  0 ,  mipHomeAddr  821012 ,  mipHomeAgent  821045 ,  mipldentification mipMHauthExtSPI mipMHauthExtAuth > $End_BehaviourLine $BehaviourLine  51 , 200 , 100 ,  test cases in  TTCN.MP  Appendix  F. 4 Typical  Control Sequences and Typical test cases in TTCN.MP  $Label $Line [5] ? RegRequest $Cref  RegRequest_216  $Verdict $Comment {  ipSourceAddr ipDestAddr mipType mipS  8285 82832  1  1  mipLifetime  10  mipHomeAddr  821012  mipHomeAgent mipCOA  821045  821020  mipldentification mipMHauthExtSPI mipMHauthExtAuth $End_BehaviourLine  $End_BehaviourDescription $End_TestCase $End_TestCases $End_DynamicPart $End_Suite  20 250 100 }  141  

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:
http://iiif.library.ubc.ca/presentation/dsp.831.1-0051178/manifest

Comment

Related Items