Řešení problému exponenciálního nárůstu stavového prostoru (state explosion) ve verifikaci protokolů chování (behavior protocols)
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F04%3A00103387" target="_blank" >RIV/67985807:_____/04:00103387 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Addresing State Explosion in Behavior Protocol Verification
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 [1]. 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, a verification tool for behavior protocols is discussed.
Název v anglickém jazyce
Addresing State Explosion in Behavior Protocol Verification
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 [1]. 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, a verification tool for behavior protocols is discussed.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
JD - Využití počítačů, robotika a její aplikace
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GA102%2F03%2F0672" target="_blank" >GA102/03/0672: Výzkum metod a nástrojů pro verifikaci odolnosti vestavěných počítačových systémů proti poruchám</a><br>
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2004
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 statě ve sborníku
Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing
ISBN
0-9700776-8-8
ISSN
—
e-ISSN
—
Počet stran výsledku
7
Strana od-do
327-333
Název nakladatele
ACIS
Místo vydání
Michigan
Místo konání akce
Beijing
Datum konání akce
30. 6. 2004
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—