Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

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

Identifikátory výsledku

  • Kód výsledku v 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>

  • Výsledek na webu

  • DOI - Digital Object Identifier

Alternativní jazyky

  • 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.

Klasifikace

  • Druh

    D - Stať ve sborníku

  • CEP obor

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

  • OECD FORD obor

Návaznosti výsledku

  • 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)

Ostatní

  • 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ů

Údaje specifické pro druh výsledku

  • 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