Publication Details

Self-healing Assurance using Bounded Model Checking

DUDKA Vendula, KŘENA Bohuslav and VOJNAR Tomáš. Self-healing Assurance using Bounded Model Checking. In: Computer Aided Systems Theory - EUROCAST 2009. Lecture Notes in Computer Science, vol. 5717. Berlin: Springer Verlag, 2009, pp. 295-303. ISBN 978-3-642-04771-8.
Czech title
Zabezpečení automatických oprav pomocí omezeného model checkingu
Type
conference paper
Language
english
Authors
Keywords

model checking, dynamic analysis, data race, concurrent Java programs, self-healing

Abstract

This paper presents an approach of using bounded model checking for healing assurance within a framework for self-healing of concurrent Java programs. In this framework, dynamic (i.e., runtime) analysis is used to detect possible data races for which some pre-defined healing strategy may subsequently be applied. Before applying such a strategy, it is desirable to confirmthat the detected possible error is indeed a real error and that the suggested healing strategy will solve it without introducing an even worse problem (namely, a deadlock). For this purpose, we suggest bounded model checking to be applied in the neighbourhood of the state in which the possible error is detected. In order to make this possible, we record certain points in the trace leading to the suspicious state within a run of the tested system, and then replay the trace in the chosen model checker (in particular, Java PathFinder) using its state space exploration capabilities to navigate between the recorded points.

Published
2009
Pages
295-303
Proceedings
Computer Aided Systems Theory - EUROCAST 2009
Series
Lecture Notes in Computer Science
Volume
5717
Conference
Twelve International Conference on Computer Aided Systems Theory---EUROCAST'09, Las Palmas de Gran Canaria, Canary Islands, ES
ISBN
978-3-642-04771-8
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX
@INPROCEEDINGS{FITPUB9017,
   author = "Vendula Dudka and Bohuslav K\v{r}ena and Tom\'{a}\v{s} Vojnar",
   title = "Self-healing Assurance using Bounded Model Checking",
   pages = "295--303",
   booktitle = "Computer Aided Systems Theory - EUROCAST 2009",
   series = "Lecture Notes in Computer Science",
   volume = 5717,
   year = 2009,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-04771-8",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9017"
}
Back to top