Verifikace protokolů chování: řešení problému

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F05%3A00031775" target="_blank" >RIV/67985807:_____/05:00031775 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

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)

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ů

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

—