About: Self-healing Assurance using Bounded Model Checking

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Self-healing Assurance using Bounded Model Checking Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	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. 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. (en)
Title	Self-healing Assurance using Bounded Model Checking Self-healing Assurance using Bounded Model Checking (en)
skos:prefLabel	Self-healing Assurance using Bounded Model Checking Self-healing Assurance using Bounded Model Checking (en)
skos:notation	RIV/00216305:26230/09:PU82666!RIV10-GA0-26230___
http://linked.open...avai/riv/aktivita	P
http://linked.open...avai/riv/aktivity	P(GA102/07/0322)
http://linked.open...vai/riv/dodaniDat	2010
http://linked.open...aciTvurceVysledku	Hrubá, Vendula Křena, Bohuslav Vojnar, Tomáš
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	340696
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/09:PU82666
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	model checking, dynamic analysis, data race, concurrent Java programs, self-healing<br> (en)
http://linked.open.../riv/klicoveSlovo	data race model checking dynamic analysis concurrent Java programs self-healing<br>
http://linked.open...ontrolniKodProRIV	[0F0F1178F24D]
http://linked.open...v/mistoKonaniAkce	Las Palmas de Gran Canaria, Canary Islands
http://linked.open...i/riv/mistoVydani	Berlin
http://linked.open...i/riv/nazevZdroje	Computer Aided Systems Theory - EUROCAST 2009
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Advanced Formal Approaches in the Design and Verification of Computer-Based Systems
http://linked.open...UplatneniVysledku	2009
http://linked.open...iv/tvurceVysledku	Hrubá, Vendula Křena, Bohuslav Vojnar, Tomáš
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2009-02-15 (xsd:date)
number of pages	9 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	978-3-642-04771-8
http://localhost/t...ganizacniJednotka	26230
is http://linked.open...avai/riv/vysledek of	Self-healing Assurance using Bounded Model Checking Self-healing Assurance using Bounded Model Checking Self-healing Assurance using Bounded Model Checking Self-healing Assurance using Bounded Model Checking

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software