D 2005

Test input generation for red-black trees using abstraction

PELÁNEK, Radek; Corina PASAREANU a Willem VISSER

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

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

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 23. 6. 2009 13:07, doc. Mgr. Radek Pelánek, Ph.D.

Anotace

ORIG CZ

V originále

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.

Č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