Test input generation for red-black trees using abstraction

PELÁNEK, Radek, Corina PASAREANU and Willem VISSER. Test input generation for red-black trees using abstraction. In Automated Software Engineering. USA: ACM, 2005, p. 414-417.

Basic information

• Original name: Test input generation for red-black trees using abstraction
• Name in Czech: Generování testovacích vstupů s využitím abstrakce
• Authors: PELÁNEK, Radek (203 Czech Republic, guarantor), Corina PASAREANU (642 Romania) and Willem VISSER (710 South Africa).
• Edition: USA, Automated Software Engineering, p. 414-417, 4 pp. 2005.
• Publisher: ACM

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: United States of America
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/05:00013479
• Organization unit: Faculty of Informatics
• Keywords in English: test input generation; state space exploration; state matching
• Tags: state matching, state space exploration, test input generation
• Tags: International impact, Reviewed

Abstract

We consider the problem of test input generation for code that manipulates complex data structures. Test inputs are sequences of method calls from the data structure interface. We describe test input input generation techniques that rely on state matching to avoid generation of redundant tests. Exhaustive techniques use explicit state model checking to explore all the possible test sequences up to predefined input sizes. Lossy techniques rely on abstraction mappings to compute and store abstract versions of the concrete states they explore under-approximations of all the possible test sequences. We have implemented the technique on top of the Java PathFinder model checker and we evaluate them using a Java implementation of red-black trees.

Abstract (in Czech)

V této práci uvažujeme problém generování testovacích vstupů pro programy, které manipulují složité datové struktury. Testovací vstupy jsou posloupnosti volání metod z rozhraní dané struktury. Popisujeme techniky, které využívají sdružování stavů k zabránění generování redundantních testů. Exhaustivní techniky používají metodu explicitního ověřování modelů k tomu, aby prozkoumali všechny posloupnosti do zadané délky. Ztrátové techniky využívají sdružování stavů pro výpočet abstraktních verzí konkrétních stavů; prozkoumávají spodní aproximace všech možných testovacích sekvencí. Implementovali jsme tyto techniky v nástroji Java PathFinder a vyhodnocujeme je na implementaci červeno-černých stromů v Javě.

Links

• GA201/03/0509, research and development project: Name: Automatizovaná verifikace paralelních a distribuovaných systémů

Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science