J 2007

Predicate Abstraction with Under-Approximation Refinement

PELÁNEK, Radek, Corina PASAREANU a Willem VISSER

Základní údaje

Originální název

Predicate Abstraction with Under-Approximation Refinement

Název česky

Predikátová abstrakce a zjemňování dolních aproximací

Autoři

PELÁNEK, Radek (203 Česká republika, garant), Corina PASAREANU (642 Rumunsko) a Willem VISSER (710 Jižní Afrika)

Vydání

Logical Methods in Computer Science, Germany, Technical University of Braunschweig, 2007, 1860-5974

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Kód RIV

RIV/00216224:14330/07:00020179

Organizační jednotka

Fakulta informatiky

UT WoS

000262497000006

Klíčová slova anglicky

model checking; predicate abstraction; under-approximation

Štítky

Příznaky

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

Anotace

ORIG CZ

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.

Česky

Navrhujeme metodu ověřování modelů založenou na abstrakci a zjemňování dolních aproximací. Metoda nevyžaduje generování abstraktních přechodů, místo toho prochází konkrétní přechody a pouze si ukládá abstraktní verze stavů specifikované abstrakčními predikáty. S využitím nástroje pro dokazování vět se automaticky kontroluje, zda při průchodu statového prostoru dochází ke ztrátě přesnosti. Aplikace metody je ilustrována na verifikaci souběžných programů.

Návaznosti

GP201/07/P035, projekt VaV
Název: Automatická analýza modelů pomocí procházení stavového prostoru
Investor: Grantová agentura ČR, Automatická analýza modelů pomocí procházení stavového prostoru
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky