Concrete Search with Abstract Matching and Refinement

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

Basic information

• Original name: Concrete Search with Abstract Matching and Refinement
• Name in Czech: Konkrétní hledání s abstraktním sdružováním a zjemněním
• Authors: PELÁNEK, Radek (203 Czech Republic, guarantor), Corina PASAREANU (642 Romania) and Willem VISSER (710 South Africa).
• Edition: Edinburgh, Computer Aided Verification, p. 52-66, 15 pp. 2005.
• Publisher: Springer

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: United Kingdom of Great Britain and Northern Ireland
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/05:00012728
• Organization unit: Faculty of Informatics
• ISBN: 3-540-27231-3
• Keywords in English: model checking; predicate abstraction; under-approximation
• Tags: Model checking, predicate abstraction, under-approximation
• Tags: International impact, Reviewed

Abstract

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.

Abstract (in Czech)

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.

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

• GD102/05/H050, research and development project: Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů

Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area 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

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware 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