Addresing State Explosion in Behavior Protocol Verification
The result's identifiers
Result code in 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>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Addresing State Explosion in Behavior Protocol Verification
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 [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.
Czech name
Řešení problému exponenciálního nárůstu stavového prostoru (state explosion) ve verifikaci protokolů chování (behavior protocols)
Czech description
Článek navrhuje reprezentaci automatů řešící problém exponenciálního nárůstu stavového prostoru (state explosion), při formální verifikaci protokolů. Tato reprezentace převádí paměťovou náročnost na časovou, ta je poté řešena dalšími optimalizacemi.
Classification
Type
D - Article in proceedings
CEP classification
JD - Use of computers, robotics and its application
OECD FORD branch
—
Result continuities
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)
Others
Publication year
2004
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing
ISBN
0-9700776-8-8
ISSN
—
e-ISSN
—
Number of pages
7
Pages from-to
327-333
Publisher name
ACIS
Place of publication
Michigan
Event location
Beijing
Event date
Jun 30, 2004
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—