Conference paperDUDKA Vendula, KŘENA Bohuslav and VOJNAR Tomáš. Using JavaPathFinder for Selfhealing Assurance. In: Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science  MEMICS 2007. Znojmo: Ing. Zdeněk Novotný, CSc., 2007, pp. 6773. ISBN 9788073550776.  Publication language:  english 

Original title:  Using JavaPathFinder for Selfhealing Assurance 

Title (cs):  Využití nástroje JavaPathFinder pro ověřování automatických oprav softwaru 

Pages:  6773 

Proceedings:  Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science  MEMICS 2007 

Conference:  MEMICS'07  3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science 

Place:  Znojmo, CZ 

Year:  2007 

ISBN:  9788073550776 

Publisher:  Ing. Zdeněk Novotný, CSc. 

Keywords 

Selfhealing, assurance, concurrency, model checking, Java PathFinder. 
Annotation 

In this paper, we deal with application of formal methods within selfhealing 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 socalled 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. 
BibTeX: 

@INPROCEEDINGS{
author = {Vendula Dudka and Bohuslav K{\v{r}}ena and Tom{\'{a}}{\v{s}}
Vojnar},
title = {Using JavaPathFinder for Selfhealing Assurance},
pages = {6773},
booktitle = {Proceedings of 3rd Doctoral Workshop on Mathematical and
Engineering Methods in Computer Science  MEMICS 2007},
year = {2007},
location = {Znojmo, CZ},
publisher = {Ing. Zden{\v{e}}k Novotn{\'{y}}, CSc.},
ISBN = {9788073550776},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=8495}
} 
