Test input generation for red-black trees using abstraction

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

Základní údaje

• Originální název: Test input generation for red-black trees using abstraction
• Název česky: Generování testovacích vstupů s využitím abstrakce
• Autoři: PELÁNEK, Radek (203 Česká republika, garant), Corina PASAREANU (642 Rumunsko) a Willem VISSER (710 Jižní Afrika).
• Vydání: USA, Automated Software Engineering, od s. 414-417, 4 s. 2005.
• Nakladatel: ACM

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Spojené státy
• Utajení: není předmětem státního či obchodního tajemství
• Kód RIV: RIV/00216224:14330/05:00013479
• Organizační jednotka: Fakulta informatiky
• Klíčová slova anglicky: test input generation; state space exploration; state matching
• Štítky: state matching, state space exploration, test input generation
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

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.

Anotace česky

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ě.

Návaznosti

• GA201/03/0509, projekt VaV: Název: Automatizovaná verifikace paralelních a distribuovaných systémů

Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů

• MSM0021622419, záměr: Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

• 1M0545, projekt VaV: Název: Institut Teoretické Informatiky

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky