Using passive testing based on symbolic execution and slicing techniques: Application to the validation of communication protocols

This paper presents a new approach to perform passive testing based on the analysis of the control and data part of the system under test. Passive testing techniques are based on the observation and verification of properties on the behaviour of a system without interfering with its normal operation. Many passive testing techniques consider only the control part of the system and neglect data, or are confronted with an overwhelming amount of data values to process. In our approach, we consider control and data parts by integrating the concepts of symbolic execution and we improve trace analysis by introducing trace slicing techniques. Properties are described using Input-Output Symbolic Transition Systems (IOSTSs) and we illustrate in the paper how they can be tested on real execution traces optimizing the trace analysis. These properties can be designed to test the functional conformance of a protocol as well as security properties. In addition to the theoretical approach, we have developed a software tool that implements the algorithms presented in this paper. Finally, as a proof of concept of our approach and tool we have applied the techniques to a real-life case study: the SIP protocol. In particular, the proposed techniques are applied to a set of real execution traces extracted from an IMS/SIP architecture.