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 | |
| Rok publikování | 2005 |
| Druh | Článek ve sborníku |
| Konference | Computer Aided Verification |
| Fakulta / Pracoviště MU | |
| 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: |
|