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”

Model checking softwarových komponent: kombinace Java PathFinder a Behavior Protocol model checker

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F06%3A00090230" target="_blank" >RIV/67985807:_____/06:00090230 - isvavai.cz</a>

  • Nalezeny alternativní kódy

    RIV/00216208:11320/07:10084051

  • Výsledek na webu

  • DOI - Digital Object Identifier

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker

  • Popis výsledku v původním jazyce

    Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled exceptions), none of them supports checking of softwarecomponents against a high-level behavior specification. We present our approach to model checking of software components implemented in Java against a high-level specification of their behavior defined via behavior protocols 1, which employs the Java PathFinder model checker and the protocol checker. The property checked by the Java PathFinder (JPF) tool (correctness of particular method call sequences) is validated via its cooperation with the protocol checker. We show that just the publisher/listenerpattern claimed to be the key flexibility support of JPF (even though proved very useful for our purpose) was not enough to achieve this kind of checking.

  • Název v anglickém jazyce

    Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker

  • Popis výsledku anglicky

    Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled exceptions), none of them supports checking of softwarecomponents against a high-level behavior specification. We present our approach to model checking of software components implemented in Java against a high-level specification of their behavior defined via behavior protocols 1, which employs the Java PathFinder model checker and the protocol checker. The property checked by the Java PathFinder (JPF) tool (correctness of particular method call sequences) is validated via its cooperation with the protocol checker. We show that just the publisher/listenerpattern claimed to be the key flexibility support of JPF (even though proved very useful for our purpose) was not enough to achieve this kind of checking.

Klasifikace

  • Druh

    D - Stať ve sborníku

  • CEP obor

    JC - Počítačový hardware a software

  • OECD FORD obor

Návaznosti výsledku

  • Projekt

    <a href="/cs/project/GA201%2F06%2F0770" target="_blank" >GA201/06/0770: Formální metody prakticky použitelné pro vývoj systémů složených ze softwarových komponent</a><br>

  • Návaznosti

    Z - Vyzkumny zamer (s odkazem do CEZ)

Ostatní

  • Rok uplatnění

    2007

  • 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

    Proceedings of 30th IEEE/NASA Software Engineering Workshop

  • ISBN

    0-7695-2624-1

  • ISSN

  • e-ISSN

  • Počet stran výsledku

    9

  • Strana od-do

    133-141

  • Název nakladatele

    IEEE Computer Society

  • Místo vydání

    Los Alamitos

  • Místo konání akce

    Loyola College Graduate Center, Columbia

  • Datum konání akce

    24. 4. 2006

  • Typ akce podle státní příslušnosti

    WRD - Celosvětová akce

  • Kód UT WoS článku