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

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

Namespace Prefixes

PrefixIRI
n21http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n20http://purl.org/net/nknouf/ns/bibtex#
n13http://localhost/temp/predkladatel/
n12http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n8http://linked.opendata.cz/resource/domain/vavai/projekt/
n17http://linked.opendata.cz/ontology/domain/vavai/
n7http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F68407700%3A21230%2F04%3A03100263%21RIV08-MPO-21230___/
n10https://schema.org/
shttp://schema.org/
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#
n14http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n19http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n9http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n5http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n11http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n18http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F68407700%3A21230%2F04%3A03100263%21RIV08-MPO-21230___
rdf:type
skos:Concept n17:Vysledek
dcterms:description
This article deals with a distributed real-time application modelling 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 tasks running under an operating system (e.g. OSEK) and using inter-task synchronization primitives. For such system, model checking algorithm implemented in a model checking tool (e.g. UPAALL) can be used to verify complex time and logical properties of the proposed model (e.g. end-to-end response time, state reachability, deadlock freeness). Since the proposed timed automata model contains more crucial details of the system behavior with respect to classical approaches to the response time analysis, the model checking approach provides less pessimistic results in many cases. Tato prace popisuje jak verifikovat rozprostrene systemy realneho casu pomoci casovanych automatu. Zamnerujeme se na systemy pouzivajici Controller Area Network (CAN) jako sbernici a predpokladame ze na kazdem CPU bezi operacni system realneho casu. Pomoci casovanych jsme schopni verifikovat nejen logicke vlastnosti, ale tez casove (uvaznuti atd.). K porovnani s tradicnimi metodami je nase metoda preciznejsi. This article deals with a distributed real-time application modelling 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 tasks running under an operating system (e.g. OSEK) and using inter-task synchronization primitives. For such system, model checking algorithm implemented in a model checking tool (e.g. UPAALL) can be used to verify complex time and logical properties of the proposed model (e.g. end-to-end response time, state reachability, deadlock freeness). Since the proposed timed automata model contains more crucial details of the system behavior with respect to classical approaches to the response time analysis, the model checking approach provides less pessimistic results in many cases.
dcterms:title
Verifikace distribuovanych systemu realneho casu casovanymi automaty. Timed Automata Approach to Real Time Distributed System Verification Timed Automata Approach to Real Time Distributed System Verification
skos:prefLabel
Timed Automata Approach to Real Time Distributed System Verification Timed Automata Approach to Real Time Distributed System Verification Verifikace distribuovanych systemu realneho casu casovanymi automaty.
skos:notation
RIV/68407700:21230/04:03100263!RIV08-MPO-21230___
n3:strany
407;410
n3:aktivita
n5:P
n3:aktivity
P(FD-K3/082)
n3:dodaniDat
n18:2008
n3:domaciTvurceVysledku
n12:8209464 n12:9687009 n12:5834805 n12:2453789
n3:druhVysledku
n11:D
n3:duvernostUdaju
n19:S
n3:entitaPredkladatele
n7:predkladatel
n3:idSjednocenehoVysledku
590364
n3:idVysledku
RIV/68407700:21230/04:03100263
n3:jazykVysledku
n9:eng
n3:klicovaSlova
Controller area network; Distributed system; Model checking; Real-Time system; Timed automata
n3:klicoveSlovo
n14:Model%20checking n14:Real-Time%20system n14:Distributed%20system n14:Timed%20automata n14:Controller%20area%20network
n3:kontrolniKodProRIV
[8CCBBFA2FCAD]
n3:mistoKonaniAkce
Vienna
n3:mistoVydani
Vienna
n3:nazevZdroje
Proceedings of 2004 IEEE International Workshop on Factory Communication Systems
n3:obor
n16:JD
n3:pocetDomacichTvurcuVysledku
4
n3:pocetTvurcuVysledku
4
n3:projekt
n8:FD-K3%2F082
n3:rokUplatneniVysledku
n18:2004
n3:tvurceVysledku
Píša, Pavel Hanzálek, Zdeněk Krákora, Jan Waszniowski, Libor
n3:typAkce
n21:WRD
n3:zahajeniAkce
2004-09-22+02:00
s:numberOfPages
4
n20:hasPublisher
IEEE Industrial Electronic Society
n10:isbn
0-7803-8734-1
n13:organizacniJednotka
21230