Name
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 confirm that 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. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-04772-5_39 | EUROCAST |
Keywords | Field | DocType |
healing assurance,bounded model checking,state space exploration capability,pre-defined healing strategy,self-healing assurance,suspicious state,possible error,possible data race,real error,chosen model checker,suggested healing strategy,state space | Self-healing,Java pathfinder,Model checking,State space exploration,Computer science,Deadlock,Theoretical computer science,Java,Java virtual machine,Bounded function | Conference |
Volume | ISSN | Citations |
5717 | 0302-9743 | 2 |
PageRank | References | Authors |
0.43 | 6 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vendula Hrubá | 1 | 10 | 1.54 |
| Bohuslav Křena | 2 | 64 | 5.15 |
| Tomáš Vojnar | 3 | 533 | 32.06 |