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:
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 |
Contact: | 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 E-mail: weiglhofer@ist.tugraz.at |
Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |