This HTML5 document contains 30 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n13http://localhost/temp/predkladatel/
n9http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n12http://linked.opendata.cz/ontology/domain/vavai/
n16http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F09%3A00047049%21RIV11-MSM-14330___/
n14http://linked.opendata.cz/resource/domain/vavai/zamer/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n4http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n11http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n10http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n5http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F09%3A00047049%21RIV11-MSM-14330___
rdf:type
skos:Concept n12:Vysledek
dcterms:description
Model checking is an increasingly popular method for formal verification of safety-critical systems. This thesis is focused on fighting state explosion (the well-known problem in model checking) by employing external memory, which can have by orders of magnitude larger capacity than internal memory. For computations, probably the most proper external memory device is hard disk. It has a sufficient speed and capacity for a low price. As a drawback, hard disks suffer from long access times, which means than data must be read by blocks in order to preserve a sufficient transfer rate. Therefore, model checking algorithms must be re-designed to behave efficiently w.r.t. the number of performed I/O operations when a substantial part of a state space is stored on disk. The thesis offers I/O-efficient solutions to the two well-known model checking problems --- reachability analysis and LTL model checking. All newly designed algorithms have been implemented, thoroughly experimentally evaluated and analysed. Model checking is an increasingly popular method for formal verification of safety-critical systems. This thesis is focused on fighting state explosion (the well-known problem in model checking) by employing external memory, which can have by orders of magnitude larger capacity than internal memory. For computations, probably the most proper external memory device is hard disk. It has a sufficient speed and capacity for a low price. As a drawback, hard disks suffer from long access times, which means than data must be read by blocks in order to preserve a sufficient transfer rate. Therefore, model checking algorithms must be re-designed to behave efficiently w.r.t. the number of performed I/O operations when a substantial part of a state space is stored on disk. The thesis offers I/O-efficient solutions to the two well-known model checking problems --- reachability analysis and LTL model checking. All newly designed algorithms have been implemented, thoroughly experimentally evaluated and analysed.
dcterms:title
External Memory LTL Model Checking External Memory LTL Model Checking
skos:prefLabel
External Memory LTL Model Checking External Memory LTL Model Checking
skos:notation
RIV/00216224:14330/09:00047049!RIV11-MSM-14330___
n3:aktivita
n10:Z n10:S
n3:aktivity
S, Z(MSM0021622419)
n3:dodaniDat
n5:2011
n3:domaciTvurceVysledku
n9:4006852
n3:druhVysledku
n15:O
n3:duvernostUdaju
n11:S
n3:entitaPredkladatele
n16:predkladatel
n3:idSjednocenehoVysledku
314453
n3:idVysledku
RIV/00216224:14330/09:00047049
n3:jazykVysledku
n7:eng
n3:klicovaSlova
LTL model checking I/O-efficient external memory flash SSD
n3:klicoveSlovo
n4:LTL%20model%20checking%20I%2FO-efficient%20external%20memory%20flash%20SSD
n3:kontrolniKodProRIV
[7AFE4027E799]
n3:obor
n17:IN
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
1
n3:rokUplatneniVysledku
n5:2009
n3:tvurceVysledku
Šimeček, Pavel
n3:zamer
n14:MSM0021622419
n13:organizacniJednotka
14330