Research On Network Protocol Testing Based On Extensions Of State Machines With Multiple Parallel Components

The conformance testing based on formal method is the basic approach to ensure reliability of network protocols. This thesis deeply studies conformance testing of new Internet protocols with some features which are hard to specify by existing formal methods.A survey is made on the related works. It is indicated that it is hard to specify the protocols with multiple parallel components sharing data via single component models or existing multiple component models. Furthermore, there is few work on formal black-box testing of software-defined networking in which there are many parallel components.In this thesis, a modeling framework on extensions of state machines with multiple parallel components is well studied. According to this framework, 3 extensions of state machines with multiple parallel components are presented. First, the PaP-EFSM(Parallel Parameterized Extended Finite State Machine), which can read external variables, is used to specify multiple parallel components communicating with shared data. Then, the PiEFSM(Pipelined Extended Finite State Machine), of which the components in same level can read and write variables and the ones in di?erent levels can delivery messages,is used to specify multi-level pipeline. Finally, the IT-EFSM(Information Table Extended Finite State Machine), which combines message communication and network topology,is presented.A DU-paths(define-use paths) based test generation method for PaP-EFSM is presented. The DU-paths for internal variables are generated and made executable. Then the DU-paths for external variables are generated. This heuristic method can be used for models with infinite variable values and no state space explosion.A Reachability Graph based hierarchical test generation method for PaP-EFSM is presented. This method can be used for models with finite variable values. It use bottomup reachability graph generation to alleviate state space explosion and top-down test generation to ensure executability of test sequences. For validation, these 2 methods stated above are applied on conformance testing of source addresses validation improvements.A test generation method for Pi-EFSM is presented. First, a data graph is extracted from model and find data paths. Then, the preambles of components on each data path are generated and composed into test sequences. Finally, the test sequences are translated into executable TTCN-3 test cases. Comparative experiment shows this method can generate test suite achieving systematical coverage of the models with acceptable cost of both time and space. For validation, this method is applied on conformance testing of OpenFlow switches. Some implementation faults and problems of protocols are revealed.A test generation method for IT-EFSM is presented. For design flaws, the modelchecking tools are used to generate counter examples from models. For implementation faults, extended test sequences are generated combining components partial composition,topology sym-simplification and simulation execution. This method can expose both design flaws and implementation faults. Furthermore, it can alleviate the risk of sate space explosion when generating tests with topology.