Řešení problému exponenciálního nárůstu stavového prostoru (state explosion) ve verifikaci protokolů chování (behavior protocols)

Kód výsledku v IS VaVaI

RIV/67985807:_____/04:00103387 - isvavai.cz

Výsledek na webu

—

DOI - Digital Object Identifier

—

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.

Druh

D - Stať ve sborníku

CEP obor

JD - Využití počítačů, robotika a její aplikace

OECD FORD obor

—

Projekt

GA102/03/0672: Výzkum metod a nástrojů pro verifikaci odolnosti vestavěných počítačových systémů proti poruchám

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

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ů

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

—