Detail publikace
Using JavaPathFinder for Self-healing Assurance
HRUBÁ, V. KŘENA, B. VOJNAR, T.
Originální název
Using JavaPathFinder for Self-healing Assurance
Anglický název
Using JavaPathFinder for Self-healing Assurance
Jazyk
en
Originální abstrakt
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.
Anglický abstrakt
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.
Dokumenty
BibTex
@inproceedings{BUT25351,
author="Vendula {Dudka} and Bohuslav {Křena} and Tomáš {Vojnar}",
title="Using JavaPathFinder for Self-healing Assurance",
annote="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.",
address="Ing. Zdeněk Novotný, CSc.",
booktitle="Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - MEMICS 2007",
chapter="25351",
howpublished="print",
institution="Ing. Zdeněk Novotný, CSc.",
year="2007",
month="october",
pages="67--73",
publisher="Ing. Zdeněk Novotný, CSc.",
type="conference paper"
}