Fault-Based Testing of Concurrent Systems

Organisation:	Institute for Software Technology / United Nations University Macau (CHINA)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Communication Protocols.
Period:	2004-2006
Size:	n/a
Description:	In fault-based testing, errors are injected into a formal specification (e.g., in LOTOS) of the system under test, generating so-called mutants, which are then used to assess or generate test cases. The quality of a test case can be assessed by counting the number of injected errors that are detected. New test cases can be obtained by guiding the execution to points where the original system behaves differently from the mutants. The overall approach is as follows: In a first step, a mutation operation is applied to the LOTOS specification, generating a mutant specification. In this case study 21 different mutation operations were used, as for instance dropping one event from a process or swapping parameters in a process call. In a second step, the LTSs (labeled transition systems) corresponding to the original specification and the mutant, are generated using CAESAR, and checked for strong bisimulation. If the two LTSs are not equivalent, use the counter example provided by CADP to extract a sequence discriminating the LTSs that can be used as test purpose. If the two LTSs are equivalent, no test case can be generated; however, investigating the reason for equivalence might help reducing redundancy in the specification. Finally, a test case is generated from the mutant specification and the test purpose, using TGV. This test case is then used to check that the implementation under test does not conform to the faulty mutant specification. This case study describes the application of fault-based testing to parts of the implementation of the HTTP protocol in the Apache web server. The LOTOS specification of the protocol was derived from the Internet standard RFC 2616, which defines the syntax and describes the semantics in natural language. Using the mutation operations, 1491 mutants were generated. Among these, 342 mutants were found to be equivalent to the original specification. For the generation of test cases, about 100 mutants were selected from the 1139 remaining mutants. Applying these tests cases to the Apache web server 2.0.40 (Red Hat Linux, HTTP/1.1 protocol) exhibited an unexpected behavior for an underspecified requirement of the standard.
Conclusions:	When applying fault injection techniques to formal specifications, the equivalence checking tools of CADP are helpful in two ways. On the one hand, if a mutant is equivalent to the original specification, understanding the reasons might help in simplifying the specification. On the other hand, the counter examples provided can be used as test purposes for which TGV can generate test cases to check an implementation.
Publications:	[Delgado-Aichernig-04] Carlo Corrales Delgado and Bernhard K. Aichernig. "Test Purpose Generation by Specification Mutation in Distributed Systems." Technical Report 313, UNU-IIST, P.O.Box 3058, Macau, September 2004. [Aichernig-Delgado-06] Bernhard K. Aichernig and Carlo Corrales Delgado. "From Faults Via Test Purposes to Test Cases: On the Fault-Based Testing of Concurrent Systems". In L. Baresi and R. Heckel (Eds.), Proceedings of the 9th International Conference on Fundamental Approaches to Software Engineering {FASE}'06 (Vienna, Austria), Lecture Notes in Computer Science, vol. 3922, pp. 324-338, Springer Verlag, March 2006. Available from the CADP Web site in PDF or PostScript
Contact:	Bernhard K. Aichernig Institute for Software Technology TU Graz Inffeldgasse 16 b A-8010 Graz AUSTRIA Tel: +43 316 873 5717 Fax: +43 316 873 5706 E-mail: aichernig@ist.tugraz.at
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page