Using JavaPathFinder for Self-healing Assurance

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F07%3APU70904" target="_blank" >RIV/00216305:26230/07:PU70904 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Using JavaPathFinder for Self-healing Assurance
Original language description
In this paper, we deal with application of formal methods within self-healing of concurrency related problems. We are currently interested in the Java programming language, and therefore we concentrate mainly on the model checker Java PathFinder (JPF). We have implemented the so-called record&replay trace strategy for navigation through a state space in order to get closer to an error state and to perform bounded model checking in the problem neighbourhood only. It allows us to increase our confidence about particular system properties in the limited time available.
Czech name
Využití nástroje JavaPathFinder pro ověřování automatických oprav softwaru
Czech description
V tomto článku se zabýváme využitím formálních metod pro ověření automatických oprav chyb souvisejících s paralelizmem. Vzhledem k tomu, že se v součanosti soustředíme na aplikace napsané v Javě, rozhodli jsme se pro model checking využívat nástroj Java PathFinder. Implementovali jsme strategii nazvanou <i>zaznamenej&přehraj</i> pro navigaci stavovým prostorem, abychom mohli provádět model checking pouze v okolí chybového stavu. To nám umožňuje v omezeném čase zvýšit naši důvěru ve správnost zvolené opravy systému.

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2007
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - MEMICS 2007
ISBN
978-80-7355-077-6
ISSN
—
e-ISSN
—
Number of pages
7
Pages from-to
67-73
Publisher name
Ing. Zdeněk Novotný, CSc.
Place of publication
Znojmo
Event location
Znojmo
Event date
Oct 26, 2007
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)