Vše
Vše

Co hledáte?

Vše
Projekty
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”

Bounded model checking v nástroji Java PathFinder

Popis výsledku

Článek se zabývá bounded model checkingem pro verifikaci programů se soubězností.

Klíčová slova

Model CheckingJava PathFinderBounded model checkingverificationRecord&Replay traceself-healingconcurrencyhealing assurance

Identifikátory výsledku

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    Bounded Model Checking Using Java PathFinder

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

    This work describes the using of bounded model checking for verification of the true races in programs. The model checking of a real system is costly, thus there are some modification or alternations of model checking of features. This paper describes the search strategy for replaying a trace and for navigating through a state space to a suspicious state and a subsequent bounded model checking initiated from this state. The bounded model checking is implemented by the model checker Java Pathfinder.

  • Název v anglickém jazyce

    Bounded Model Checking Using Java PathFinder

  • Popis výsledku anglicky

    This work describes the using of bounded model checking for verification of the true races in programs. The model checking of a real system is costly, thus there are some modification or alternations of model checking of features. This paper describes the search strategy for replaying a trace and for navigating through a state space to a suspicious state and a subsequent bounded model checking initiated from this state. The bounded model checking is implemented by the model checker Java Pathfinder.

Klasifikace

  • Druh

    D - Stať ve sborníku

  • CEP obor

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

  • OECD FORD obor

Návaznosti výsledku

Ostatní

  • Rok uplatnění

    2008

  • 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 the 14th Conference STUDENT EEICT 2008

  • ISBN

    978-80-214-3615-2

  • ISSN

  • e-ISSN

  • Počet stran výsledku

    3

  • Strana od-do

  • Název nakladatele

    Brno University of Technology

  • Místo vydání

    Brno

  • Místo konání akce

    FEKT VUT v Brně

  • Datum konání akce

    24. 4. 2008

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

    CST - Celostátní akce

  • Kód UT WoS článku

Základní informace

Druh výsledku

D - Stať ve sborníku

D

CEP

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

Rok uplatnění

2008