Behavior Protocol Verification: Fighting State Explosion

Kód výsledku v IS VaVaI

RIV/00216208:11320/05:00207528 - isvavai.cz

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Behavior Protocol Verification: Fighting State Explosion

Popis výsledku v původním jazyce

Annotation in the original language is: 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 state spaces 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

Behavior Protocol Verification: Fighting State Explosion

Popis výsledku anglicky

Annotation in the original language is: 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 state spaces 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

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

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
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

1646-3692

e-ISSN

—

Svazek periodika

2005

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

9

Strana od-do

—

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—