Attributes | Values |
---|
rdf:type
| |
Description
| - V tomto článku se zabýváme využitím formálních metod pro ověření automatických oprav chyb souvisejících s paralelizmem. Vzhledem k tomu, že se v součanosti soustředíme na aplikace napsané v Javě, rozhodli jsme se pro model checking využívat nástroj Java PathFinder. Implementovali jsme strategii nazvanou <i>zaznamenej&přehraj</i> pro navigaci stavovým prostorem, abychom mohli provádět model checking pouze v okolí chybového stavu. To nám umožňuje v omezeném čase zvýšit naši důvěru ve správnost zvolené opravy systému. (cs)
- In this paper, we deal with application of formal methods within self-healing of concurrency related problems. We are currently interested in the Java programming language, and therefore we concentrate mainly on the model checker Java PathFinder (JPF). We have implemented the so-called record&replay trace strategy for navigation through a state space in order to get closer to an error state and to perform bounded model checking in the problem neighbourhood only. It allows us to increase our confidence about particular system properties in the limited time available.
- In this paper, we deal with application of formal methods within self-healing of concurrency related problems. We are currently interested in the Java programming language, and therefore we concentrate mainly on the model checker Java PathFinder (JPF). We have implemented the so-called record&replay trace strategy for navigation through a state space in order to get closer to an error state and to perform bounded model checking in the problem neighbourhood only. It allows us to increase our confidence about particular system properties in the limited time available. (en)
|
Title
| - Using JavaPathFinder for Self-healing Assurance
- Using JavaPathFinder for Self-healing Assurance (en)
- Využití nástroje JavaPathFinder pro ověřování automatických oprav softwaru (cs)
|
skos:prefLabel
| - Using JavaPathFinder for Self-healing Assurance
- Using JavaPathFinder for Self-healing Assurance (en)
- Využití nástroje JavaPathFinder pro ověřování automatických oprav softwaru (cs)
|
skos:notation
| - RIV/00216305:26230/07:PU70904!RIV08-MSM-26230___
|
http://linked.open.../vavai/riv/strany
| |
http://linked.open...avai/riv/aktivita
| |
http://linked.open...avai/riv/aktivity
| - P(GA102/07/0322), P(GP102/06/P076), Z(MSM0021630528)
|
http://linked.open...vai/riv/dodaniDat
| |
http://linked.open...aciTvurceVysledku
| |
http://linked.open.../riv/druhVysledku
| |
http://linked.open...iv/duvernostUdaju
| |
http://linked.open...titaPredkladatele
| |
http://linked.open...dnocenehoVysledku
| |
http://linked.open...ai/riv/idVysledku
| - RIV/00216305:26230/07:PU70904
|
http://linked.open...riv/jazykVysledku
| |
http://linked.open.../riv/klicovaSlova
| - Self-healing, assurance, concurrency, ,model checking, Java PathFinder. (en)
|
http://linked.open.../riv/klicoveSlovo
| |
http://linked.open...ontrolniKodProRIV
| |
http://linked.open...v/mistoKonaniAkce
| |
http://linked.open...i/riv/mistoVydani
| |
http://linked.open...i/riv/nazevZdroje
| - Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - MEMICS 2007
|
http://linked.open...in/vavai/riv/obor
| |
http://linked.open...ichTvurcuVysledku
| |
http://linked.open...cetTvurcuVysledku
| |
http://linked.open...vavai/riv/projekt
| |
http://linked.open...UplatneniVysledku
| |
http://linked.open...iv/tvurceVysledku
| - Hrubá, Vendula
- Křena, Bohuslav
- Vojnar, Tomáš
|
http://linked.open...vavai/riv/typAkce
| |
http://linked.open.../riv/zahajeniAkce
| |
http://linked.open...n/vavai/riv/zamer
| |
number of pages
| |
http://purl.org/ne...btex#hasPublisher
| |
https://schema.org/isbn
| |
http://localhost/t...ganizacniJednotka
| |