2005
Concrete Search with Abstract Matching and Refinement
PELÁNEK, Radek; Corina PASAREANU and Willem VISSERBasic 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
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
International impact, Reviewed
Changed: 21/11/2006 14:02, doc. Mgr. Radek Pelánek, Ph.D.
In the original language
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.
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 |
| ||
| GD102/05/H050, research and development project |
| ||
| MSM0021622419, plan (intention) |
| ||
| 1ET408050503, research and development project |
| ||
| 1M0545, research and development project |
|