Under-Approximation Generation using Partial Order Reduction

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. Under-Approximation Generation using Partial Order Reduction. Brno: Faculty of Informatics, 2005, 21 s. Technical Reports, FIMU-RS-2005-04.

Základní údaje

• Originální název: Under-Approximation Generation using Partial Order Reduction
• Název česky: Generování stavového prostoru s použitím under-aproximace a partial order reduction
• Autoři: BRIM, Luboš (203 Česká republika, garant), Ivana ČERNÁ (203 Česká republika), Pavel MORAVEC (203 Česká republika) a Jiří ŠIMŠA (203 Česká republika).
• Vydání: Brno, 21 s. Technical Reports, FIMU-RS-2005-04, 2005.
• Nakladatel: Faculty of Informatics

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Odborná kniha
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• WWW: URL
• Kód RIV: RIV/00216224:14330/05:00012458
• Organizační jednotka: Fakulta informatiky
• Klíčová slova anglicky: under-aproximation; state space generation; partial order reduction
• Štítky: partial order reduction, state space generation, under-aproximation
• Příznaky: Mezinárodní význam

Anotace

We propose a new on-the-fly approach which combines partial order reduction with the under-approximation technique for falsification and verification of LTL-X properties. It uses sensitivity relation and modified ample conditions to generate a reduced state space that is not fully stutter equivalent to the original one and it checks the desired property using representatives. Widening of under-approximations is fully automatic and does not rely on any supporting mechanisms like theorem-provers or SAT solvers.

Anotace česky

V práci je navržen nový způsob generování stavových prostorů kombinující metody partial order reduction s under-approximacemi pro ověřování LTL-X vlastností modelu. Používá relaci sensitivity a modifikované podmínky na ample-sets. Výsledný redukovaný stavový prostor není plně ekvivalentní původnímu, v práci jsou proto navrženy rozšíření under-aproximací, které lze provádět automaticky a nepotřebují další pomocné mechanismy jako jsou theorem-proovers nebo SAT solvery.

Návaznosti

• GA201/03/0509, projekt VaV: Název: Automatizovaná verifikace paralelních a distribuovaných systémů

Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů