Formal approaches provide many keys to efficiently test the confor- mance of communicating protocols. Active and passive testing techniques are two main sets of these approaches. Compare to active testing, passive testing techniques are used whenever the system cannot be interrupted, or its interfaces are unavailable to access. Under such conditions, communication traces are ex- tracted from points of observation and compared with the expected conformance requirements formally specified as properties. This paper presents a novel mon- itoring approach, aiming at formally specifying protocol properties in order to check them on real execution traces. A prototype is developed and experienced based on the algorithms defined in a previous paper. Experiments are presented through a set of IMS/SIP properties and numerous execution traces in order to evaluate and assess our technique. The relevant verdicts and discussions are pro- vided at the end. Two main types of formal approaches can be applied to test the conformance of commu- nicating protocols: active and passive testing. While active testing techniques are based on the analysis of the protocol answers when it is stimulated, the passive ones focus on the observation of input and output events of the implementation under test (IUT) in run-time. They are called passive since they do not modify the runtime behavior of the IUT. Although passive testing does lack some of the advantages of active techniques, such as test coverage, it provides an effective tool for fault detection when the access to the interfaces of the system is unavailable, or in already deployed systems, where the system cannot be interrupted. In order to check conformance of the IUT, the record of the observation during runtime (called trace) is compared with the expected behavior, defined by either a formal model (1) (when available) or as a set of formally specified properties (2) obtained from the requirements of the protocol. In the context of black-box testing of communicating protocols, executions of the system are limited to communication traces, i.e. inputs and outputs to and from the IUT. Since passive testing approaches derive from model-based methodologies (3), such in- put/output events are usually modeled as: a control part, an identifier for the event be- longing to a finite set, and a data part, a set of parameters accompanying the control
['Xiaoping Che', 'Felipe Lalanne', 'Stephane Maag']
A Formal Monitoring Technique for SIP Conformance Testing