Verifikace protokolů chování: řešení problému
Popis výsledku
Typický problém při použití techniky automatického ověřování je velikost stavového prostoru. Dokonce i v případě malého systému narůstá stavový prostor exponenciálně (problém "state explosion"). V tomto článku prezentujeme novou reprezentaci stavového prostoru pro implementaci operací nad protokoly chování softwarových komponent. Navrhovaná repreyentace je lineární vzhledem k velikosti protokolu chování. Omezení prostorové náročnosti při nárustu časové náročnosti umožňuje verifikaci prokotolů praktickévelikosti. Jako důkaz použitelnosti nové reprezentace diskutujeme dvě verze nástroje pro verifikaci.
Klíčová slova
formal verificationsoftware componentsstateexplos ionbehavior protocolsparse trees
Identifikátory výsledku
Kód výsledku v IS VaVaI
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Behaviout Protocols Verification: Fighting State Explosion
Popis výsledku v původním jazyce
A typical problem formal verification faces is the size of the model of a system being verified. Even for a small system, the state space of the model tends to grow exponentially (state explosion). In this paper, we present a new representation of statespaces suitable for implementing operations upon behavior protocols of software components. The proposed representation is linear in length of the source behavior protocol. By trading space for time, it allows handling behavior protocols of "practical size". As a proof of concept, two versions of a verification tool based on the proposed technique are discussed.
Název v anglickém jazyce
Behaviout Protocols Verification: Fighting State Explosion
Popis výsledku anglicky
A typical problem formal verification faces is the size of the model of a system being verified. Even for a small system, the state space of the model tends to grow exponentially (state explosion). In this paper, we present a new representation of statespaces suitable for implementing operations upon behavior protocols of software components. The proposed representation is linear in length of the source behavior protocol. By trading space for time, it allows handling behavior protocols of "practical size". As a proof of concept, two versions of a verification tool based on the proposed technique are discussed.
Klasifikace
Druh
Jx - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2005
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název periodika
International Journal of Computer and Information Science
ISSN
1525-9293
e-ISSN
—
Svazek periodika
6
Číslo periodika v rámci svazku
2
Stát vydavatele periodika
US - Spojené státy americké
Počet stran výsledku
10
Strana od-do
22-30
Kód UT WoS článku
—
EID výsledku v databázi Scopus
—
Druh výsledku
Jx - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP
JC - Počítačový hardware a software
Rok uplatnění
2005