About: Distributed Explicit Bounded LTL Model Checking

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

About: Distributed Explicit Bounded 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	Automated formal verification becomes a significant part of an industrial design process. Favourite formal verification method - model checking - is strongly limited by the size of the model of the verified system. It suffers from the so called state explosion problem. We propose to fight this problem by applying the idea of bounding the examined state space in explicit model checking. Moreover, we combine this approach with the distribution of the computation among the network of workstations. We consider several distributed bounded LTL model checking algorithms and carry out a series of experiments to evaluate them and to compare their behaviour. Automated formal verification becomes a significant part of an industrial design process. Favourite formal verification method - model checking - is strongly limited by the size of the model of the verified system. It suffers from the so called state explosion problem. We propose to fight this problem by applying the idea of bounding the examined state space in explicit model checking. Moreover, we combine this approach with the distribution of the computation among the network of workstations. We consider several distributed bounded LTL model checking algorithms and carry out a series of experiments to evaluate them and to compare their behaviour. (en) Automated formal verification becomes a significant part of an industrial design process. Favourite formal verification method - model checking - is strongly limited by the size of the model of the verified system. It suffers from the so called state explosion problem. We propose to fight this problem by applying the idea of bounding the examined state space in explicit model checking. Moreover, we combine this approach with the distribution of the computation among the network of workstations. We consider several distributed bounded LTL model checking algorithms and carry out a series of experiments to evaluate them and to compare their behaviour. (cs)
Title	Distributed Explicit Bounded LTL Model Checking Distributed Explicit Bounded LTL Model Checking (en) Distributed Explicit Bounded LTL Model Checking (cs)
skos:prefLabel	Distributed Explicit Bounded LTL Model Checking Distributed Explicit Bounded LTL Model Checking (en) Distributed Explicit Bounded LTL Model Checking (cs)
skos:notation	RIV/00216224:14330/03:00008587!RIV08-MSM-14330___
http://linked.open.../vavai/riv/strany	30
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(GA201/03/0509), Z(MSM 143300001)
http://linked.open...vai/riv/dodaniDat	2008
http://linked.open...aciTvurceVysledku	Krčál, Pavel
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	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	604122
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/03:00008587
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Distributed Algorithms; LTL Model Checking; Bounded Model Checking (en)
http://linked.open.../riv/klicoveSlovo	LTL Model Checking Bounded Model Checking Distributed Algorithms
http://linked.open...ontrolniKodProRIV	[CB317572282F]
http://linked.open...v/mistoKonaniAkce	Boulder, Colorado, USA
http://linked.open...i/riv/mistoVydani	Neuveden
http://linked.open...i/riv/nazevZdroje	Second International Workshop on Parallel and Distributed Model Checking
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...vavai/riv/projekt	Automated Verification of Parallel and Distributed Systems
http://linked.open...UplatneniVysledku	2003
http://linked.open...iv/tvurceVysledku	Krčál, Pavel
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2003-01-01 (xsd:date)
http://linked.open...n/vavai/riv/zamer	http://linked.opendata.cz/resource/domain/vavai/zamer/MSM%20143300001
number of pages	18 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Elsevier
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, 47 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software