This HTML5 document contains 37 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/
n11http://localhost/temp/predkladatel/
n6http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n5http://linked.opendata.cz/resource/domain/vavai/projekt/
n15http://linked.opendata.cz/ontology/domain/vavai/
n14http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F68407700%3A21230%2F05%3A00110220%21RIV14-MSM-21230___/
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#
n10http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n8http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n16http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n4http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F68407700%3A21230%2F05%3A00110220%21RIV14-MSM-21230___
rdf:type
skos:Concept n15:Vysledek
dcterms:description
This article deals with a distributed, fault-tolerant real-time application modeling by timed automata. The application under consideration consists of several processors communicating via Controller Area Network (CAN); each processor executes an application that consists of fault-tolerant tasks running under an operating system (e.g. OSEK) and using inter-task synchronization primitives. For such system, the model checking tool (e.g. UPAALL) can be used to verify complex time and logical properties formalized as a safety or bounded liveness properties (e.g. end-to-end response time considering occurrence of a fault, state reachability).The main contribution of this paper is that the proposed model reduces size of the state-space by sharing clocks measuring the execution time of tasks and simply incorporates fault-tolerant features of the application. This article deals with a distributed, fault-tolerant real-time application modeling by timed automata. The application under consideration consists of several processors communicating via Controller Area Network (CAN); each processor executes an application that consists of fault-tolerant tasks running under an operating system (e.g. OSEK) and using inter-task synchronization primitives. For such system, the model checking tool (e.g. UPAALL) can be used to verify complex time and logical properties formalized as a safety or bounded liveness properties (e.g. end-to-end response time considering occurrence of a fault, state reachability).The main contribution of this paper is that the proposed model reduces size of the state-space by sharing clocks measuring the execution time of tasks and simply incorporates fault-tolerant features of the application.
dcterms:title
Timed Automata Approach to Distributed and Fault Tolerant System Verification Timed Automata Approach to Distributed and Fault Tolerant System Verification
skos:prefLabel
Timed Automata Approach to Distributed and Fault Tolerant System Verification Timed Automata Approach to Distributed and Fault Tolerant System Verification
skos:notation
RIV/68407700:21230/05:00110220!RIV14-MSM-21230___
n3:aktivita
n12:P
n3:aktivity
P(1M0567)
n3:dodaniDat
n4:2014
n3:domaciTvurceVysledku
n6:2453789 n6:5834805 n6:9687009
n3:druhVysledku
n17:O
n3:duvernostUdaju
n8:S
n3:entitaPredkladatele
n14:predkladatel
n3:idSjednocenehoVysledku
546824
n3:idVysledku
RIV/68407700:21230/05:00110220
n3:jazykVysledku
n16:eng
n3:klicovaSlova
Controller area network; Distributed system; Model checking; Real-Time system; Timed automata
n3:klicoveSlovo
n10:Model%20checking n10:Distributed%20system n10:Real-Time%20system n10:Controller%20area%20network n10:Timed%20automata
n3:kontrolniKodProRIV
[E2F56D3D2C47]
n3:obor
n13:JD
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
3
n3:projekt
n5:1M0567
n3:rokUplatneniVysledku
n4:2005
n3:tvurceVysledku
Hanzálek, Zdeněk Waszniowski, Libor Krákora, Jan
n11:organizacniJednotka
21230