Database of Case Studies Achieved Using CADP

Model-Based Testing of Registrar Entity for the Session Initiation Protocol

Organisation: Technical University of Graz

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Communication Protocols.

Period: 2007

Size: 3,000 lines of LOTOS: 20 data types (2,500 lines of LOTOS) and 10 processes

Description: This case study aims at testing the conformance of two implementations of the SIP (Session Initiation Protocol) Registrar in the context of a VoIP (Voice over IP) server.

First, a formal specification of the SIP registrar is derived from its natural language definition (RFC 3261), using thirteen abstractions that allow to reduce the complexity of the system whilst preserving the properties of interest; for instance, only three different users are considered. These abstractions have been thoroughly reviewed and approved by domain experts.

Second, two strategies are applied to design a set of test purposes:

  • The first strategy is based on structural covering criteria (e.g., decision/condition coverage). Test purposes designed using this approach usually overlap, i.e., the generated test graphs have (many) common traces, leading to many different test cases detecting the same errors. To reduce this overlap, test purposes containing similar edges were merged manually.

  • The second strategy is based on fault models (i.e., anticipating defects based on domain knowledge and previously made errors), extending the approach described in the CADP case study "Fault-Based Testing of Concurrent Systems" (injection of faults by mutation of the specification and using as test purpose the counter example provided by the BISIMULATOR tool of CADP when comparing the original specification with the mutated one) so as to apply the mutation and the BISIMULATOR tool only on those parts of the specification affected by the mutation. This improves the scalability of the approach and enables to handle larger specifications.

Third, these sets of test purposes are used to generate with the TGV tool a set of abstract test cases still containing the abstraction made by the LOTOS specification. The execution of these test cases is performed within the abstract test execution framework, taking charge of the transformations between abstract stimuli and concrete protocol messages.

Finally, the generated test cases were used to check the conformance of two implementations of the SIP registrar, in both of which errors have been detected. The test cases obtained using structural criteria allowed to find nine errors in a commercial implementation and four errors in the OpenSER implementation. The test cases obtained using the fault-based approach allowed to detect an additional error in the commercial implementation.

Conclusions: Automatic test case generation based on a LOTOS model of the registrar entity allowed to discover that two implementations of the registrar violate the current definition (RFC 3261) in several respects (ten violations for a commercial implementation and four violations for OpenSER).

Publications: [Aichernig-Weiglhofer-Peischl-Wotawa-07-a] Bernhard K. Aichernig, Martin Weiglhofer, Bernhard Peischl, and Franz Wotawa. "Test Purpose Generation in an Industrial Application". In Proceedings of the 3rd International Workshop on Advances in Model-Based Testing, pp. 115-125, ACM, July 2007.

[Aichernig-Weiglhofer-Peischl-Wotawa-07-b] Bernhard K. Aichernig, Martin Weiglhofer, Bernhard Peischl, Franz Wotawa. "Protocol Conformance Testing a SIP Registrar: an Industrial Application of Formal Methods". In Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods SEFM 2007 (London, United Kingdom), pp. 215-226, IEEE Computer Society Press, September 2007.
Available on-line from the CADP Web site in PDF or PostScript

[Aichernig-Weiglhofer-Wotawa-08] Bernhard K. Aichernig, Martin Weiglhofer, and Franz Wotawa "Improving Fault-based Conformance Testing". In Bernd Finkbeiner, Yuri Gurevich and Alexander K. Petrenko editors, Proceedings of the 4th International Workshop on Model-Based Testing {MBT}'2008 (Budapest, Hungary) , Electronic Notes in Theoretical Computer Science, volume 220, pp. 63-77, March 2008.
Available on-line from the CADP Web site in PDF or PostScript
Martin Weiglhofer
Competence Network Softnet Austria
Institute for Software Technology
Technische Universität Graz
8010 Graz, Austria
Tel: +43 316 873 5736
Fax: +43 316 873 5706

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Mon Jul 4 11:04:00 2022.

Back to the CADP case studies page