Concrete Search with Abstract Matching and Refinement

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Konkrétní hledání s abstraktním sdružováním a zjemněním
Autoři

PELÁNEK Radek PASAREANU Corina VISSER Willem

Rok publikování 2005
Druh Článek ve sborníku
Konference Computer Aided Verification
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova model checking; predicate abstraction; under-approximation
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.