Detail publikačního výsledku

Self-healing Assurance using Bounded Model Checking

DUDKA, V.; KŘENA, B.; VOJNAR, T.

Originální název

Self-healing Assurance using Bounded Model Checking

Anglický název

Self-healing Assurance using Bounded Model Checking

Druh

Stať ve sborníku mimo WoS a Scopus

Originální abstrakt

This paper presents an approach of using bounded model checkingfor 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 navigatebetween the recorded points.

Anglický abstrakt

This paper presents an approach of using bounded model checkingfor 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 navigatebetween the recorded points.

Klíčová slova

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

Klíčová slova v angličtině

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

Autoři

DUDKA, V.; KŘENA, B.; VOJNAR, T.

Rok RIV

2010

Vydáno

06.09.2009

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-642-04771-8

Kniha

Computer Aided Systems Theory - EUROCAST 2009

Edice

Lecture Notes in Computer Science

Svazek

5717

Strany od

295

Strany do

303

Strany počet

9

BibTex

@inproceedings{BUT34283,
  author="Vendula {Dudka} and Bohuslav {Křena} and Tomáš {Vojnar}",
  title="Self-healing Assurance using Bounded Model Checking",
  booktitle="Computer Aided Systems Theory - EUROCAST 2009",
  year="2009",
  series="Lecture Notes in Computer Science",
  volume="5717",
  pages="295--303",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-642-04771-8"
}