Concrete Search with Abstract Matching and Refinement

PELÁNEK, Radek, Corina PASAREANU a Willem VISSER. Concrete Search with Abstract Matching and Refinement. In Computer Aided Verification. Edinburgh: Springer, 2005, s. 52-66. ISBN 3-540-27231-3.

Základní údaje

• Originální název: Concrete Search with Abstract Matching and Refinement
• Název česky: Konkrétní hledání s abstraktním sdružováním a zjemněním
• Autoři: PELÁNEK, Radek (203 Česká republika, garant), Corina PASAREANU (642 Rumunsko) a Willem VISSER (710 Jižní Afrika).
• Vydání: Edinburgh, Computer Aided Verification, od s. 52-66, 15 s. 2005.
• Nakladatel: Springer

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Velká Británie a Severní Irsko
• Utajení: není předmětem státního či obchodního tajemství
• Kód RIV: RIV/00216224:14330/05:00012728
• Organizační jednotka: Fakulta informatiky
• ISBN: 3-540-27231-3
• Klíčová slova anglicky: model checking; predicate abstraction; under-approximation
• Štítky: Model checking, predicate abstraction, under-approximation
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while storing abstract versions of the concrete states, as specified by a set of abstraction predicates. For each explored transition the method checks, with the help of a theorem prover, whether there is any loss of precision introduced by abstraction. The results of these checks are used to decide termination or to refine the abstraction by generating new abstraction predicates. If the (possibly infinite) concrete system under analysis has a finite bisimulation quotient, then the method is guaranteed to eventually explore an equivalent finite bisimilar structure. We illustrate the application of the approach for checking concurrent programs. We also show how a lightweight variant can be used for efficient software testing.

Anotace česky

Navrhujeme novou metodu pro ověřování modelu pomocí abstrakce založenou na zjemňování spodních aproximací všech možných chování zadaného systému. Metoda zachovává všechny chyby vzhledem k vlastnostem typu bezpečnost, protože všechna analyzovaná chování jsou z definice realizovatelná. Metoda nevyžaduje generování abstraktního přechodového systému, ale spouští konkrétní přechody, přičemž ukládá abstraktní verze nalezených stavů. Tato abstrakce je vypočítána pomocí zadaných predikátů. Pro každý prozkoumaný přechod metoda ověří (s využitím nástroje pro dokazování vět), zda došlo ke ztrátě přesnosti díky abstrakci. Výsledky těchto testů jsou využity pro rozhodnutí ukončení metody nebo pro zavedení nových predikátů. Pokud má zadaný systém (potenciálně nekonečně-stavový) konečný bisimulační kolaps, pak můžeme garantovat, že metoda eventuálně prozkoumá konečnou bisimilární strukturu. Ilustrujeme tento nový přístup na aplikaci pro paralelní programy. Ukazujeme též odlehčenou variantu metody, která může být použita pro efektivní testování softwaru.

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ů

• GD102/05/H050, projekt VaV: Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů

Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti 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

• 1ET408050503, projekt VaV: Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů

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

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