About: External Memory LTL Model Checking

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

About: External Memory LTL 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	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. (en)
Title	External Memory LTL Model Checking External Memory LTL Model Checking (en)
skos:prefLabel	External Memory LTL Model Checking External Memory LTL Model Checking (en)
skos:notation	RIV/00216224:14330/09:00047049!RIV11-MSM-14330___
http://linked.open...avai/riv/aktivita	S Z
http://linked.open...avai/riv/aktivity	S, Z(MSM0021622419)
http://linked.open...vai/riv/dodaniDat	2011
http://linked.open...aciTvurceVysledku	Šimeček, Pavel
http://linked.open.../riv/druhVysledku	O - Ostatní výsledky nezařaditelné do žádného z výše uvedených druhů výsledku
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	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	314453
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/09:00047049
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	LTL model checking I/O-efficient external memory flash SSD (en)
http://linked.open.../riv/klicoveSlovo	LTL model checking I/O-efficient external memory flash SSD
http://linked.open...ontrolniKodProRIV	[7AFE4027E799]
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	1 (xsd:int)
http://linked.open...UplatneniVysledku	2009
http://linked.open...iv/tvurceVysledku	Šimeček, Pavel
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
http://localhost/t...ganizacniJednotka	14330

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