Research On Distributed Protocol Interoperability Testing Based On Formal Methods

Most network protocols have the distributed nature, so it is necessary for distributed protocol implementations located in different network devices to work together and perform protocol functions. Protocol interoperability testing is an important technique to ensure protocol implementations located in different network devices working together correctly. The purpose of interoperability testing is to test whether two or more protocol implementations can communicate with each other correctly and interoperate as a whole system to perform functions specified in protocol specifications. Based on formal methods, this thesis deeply studies distributed protocol interoperability testing. Main contents and conclusions of this thesis are as follows.A survey is made on the research of protocol interoperability testing and distributed testing. It is indicated that in the existing works only the simple situation of one against one is considered, but more generic situations such as one against N are not considered.In this thesis, a generic theoretical framework of interoperability testing is established. Firstly, the abstract model of system under test is defined; after introducing the abstract concept of interoperability relation, the formal definitions of the whole processes of interoperability testing are given. Communicating Multi-port Finite State Machines (CMpFSM) is used to specify the behaviors of inputs and outputs; furthermore for protocols with time constraints, the model Communicating Multi-port Timed Input Output Automata (CMpTIOA) is used; then the definitions of interoperability relations are also redefined for the two models to act as test purposes.A distributed interoperability test generation method by using multiple testers is presented. Firstly, global test sequences are generated from CMpFSM model of system under test; in order to improve the fault coverage, an enhanced test generation method is presented; then, suitable distributed test architecture is selected and a formal algorithm is presented to distribute the global test sequences to different testers and generate distributed synchronizable test suite.Time constraints are important factors in network protocols. This thesis deeply studies interoperability testing considering time constraints in protocols. Firstly, a test generation method based on timed interoperability relation is proposed. A mechanism of executability pre-determination is also integrated in the test generation method. The results of this method are parameterized test behavior trees. This method alleviates state explosion problem to some extent. Then, two real-time test notations-- real-time TTCN and TIMEDTTCN-3 are investigated. Transformation methods are given to convert test behavior trees to real-time test notations. Since real-time TTCN has not enough capabilities of specifying time constraints in real-time interoperability testing, an extension of real-time TTCN is proposed to fill in such a gap.Test execution subsystems based on the two real-time test notations are designed and implemented, and the initial prototypes of test systems are constructed. The proposed theory and methods have been appled in the interoperability testing of the next generation Internet protocols (IPv6).