A Formal Approach to Robustness Testing of Network Protocol with Time Constraints

Network protocols often have time constraints. Robustness testing of protocol with time constraints aims to detect vulnerabilities of its implementation. However, related theory is not well developed. This paper proposes a novel Timed NPEFSM model containing sufficient inputs with various time values and their processing rules to formalize protocol with time constraints. In order to test delay transitions, Grid Timed NPEFSM is proposed which can be generated by state characterization of Timed NPEFSM using time sampling. Thus, these two models jointly guide robustness testing of protocol with time constraints. For test generation, we propose timed anomalous test case in which only state under test is characterized by time sampling and this method can simplify test sequences largely without compromising test coverage. We also propose several strategies to construct timed test sequences. To inject test data efficiently and effectively, three types of timed compound anomalous test cases are proposed. Standard test specification language TTCN-3 is extended to describe test generation. We illustrate our method using a routing protocol: OSPFv2.