Predicate Abstraction with Under-Approximation Refinement

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F07%3A00020179" target="_blank" >RIV/00216224:14330/07:00020179 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Predicate Abstraction with Under-Approximation Refinement

Original language description

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 feasibleby 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 th

Czech name

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

Czech description

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ů.

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

IN - Informatics

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2007

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Logical Methods in Computer Science

ISSN

1860-5974

e-ISSN

—

Volume of the periodical

3

Issue of the periodical within the volume

1

Country of publishing house

DE - GERMANY

Number of pages

22

Pages from-to

1-22

UT code for WoS article

—

EID of the result in the Scopus database

—