B 2005

Under-Approximation Generation using Partial Order Reduction

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA

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

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í

Odkazy

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

Příznaky

Mezinárodní význam
Změněno: 19. 12. 2006 13:19, prof. RNDr. Luboš Brim, CSc.

Anotace

ORIG CZ

V originále

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.

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