Publication detail

Self-healing Assurance using Bounded Model Checking

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

Original Title

Self-healing Assurance using Bounded Model Checking

English Title

Self-healing Assurance using Bounded Model Checking

Type

conference paper

Language

en

Original 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.

English 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.

Keywords

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

RIV year

2009

Released

06.09.2009

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-642-04771-8

Book

Computer Aided Systems Theory - EUROCAST 2009

Edition

Lecture Notes in Computer Science

Edition number

NEUVEDEN

Pages from

295

Pages to

303

Pages count

9

Documents

BibTex


@inproceedings{BUT34283,
  author="Vendula {Dudka} and Bohuslav {Křena} and Tomáš {Vojnar}",
  title="Self-healing Assurance using Bounded Model Checking",
  annote="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.",
  address="Springer Verlag",
  booktitle="Computer Aided Systems Theory - EUROCAST 2009",
  chapter="34283",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  journal="Lecture Notes in Computer Science (IF 0,513)",
  year="2009",
  month="september",
  pages="295--303",
  publisher="Springer Verlag",
  type="conference paper"
}