Behaviout Protocols Verification: Fighting State Explosion

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Behaviout Protocols Verification: Fighting State Explosion

Original language description

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.

Czech name

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

Czech description

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.

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/GA102%2F03%2F0672" target="_blank" >GA102/03/0672: Research of methods and tools for verification of embedded computer system fault tolerance</a><br>

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2005

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

International Journal of Computer and Information Science

ISSN

1525-9293

e-ISSN

—

Volume of the periodical

6

Issue of the periodical within the volume

2

Country of publishing house

US - UNITED STATES

Number of pages

10

Pages from-to

22-30

UT code for WoS article

—

EID of the result in the Scopus database

—