2005
Concrete Search with Abstract Matching and Refinement
PELÁNEK, Radek, Corina PASAREANU a Willem VISSERZá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
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
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 21. 11. 2006 14:02, doc. Mgr. Radek Pelánek, Ph.D.
V originále
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.
Č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 |
| ||
| GD102/05/H050, projekt VaV |
| ||
| MSM0021622419, záměr |
| ||
| 1ET408050503, projekt VaV |
| ||
| 1M0545, projekt VaV |
|