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

Statements

Subject Item
n2:RIV%2F68407700%3A21230%2F05%3A03110427%21RIV06-AV0-21230___
rdf:type
n10:Vysledek skos:Concept
dcterms:description
The aim of this article is to show, how a multitasking application running under real-time operating system compliant with OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several tasks, it includes resource sharing and synchronization by events. For such system, we use model checking theory based on timed automata and we verify time and logical properties of proposed model by existing model checking tools. Since a complexity of the model-checking verification exponentially grows with the number of clocks used in a model, the proposed model uses only one clock for measuring execution time of all modeled tasks. Není k dispozici The aim of this article is to show, how a multitasking application running under real-time operating system compliant with OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several tasks, it includes resource sharing and synchronization by events. For such system, we use model checking theory based on timed automata and we verify time and logical properties of proposed model by existing model checking tools. Since a complexity of the model-checking verification exponentially grows with the number of clocks used in a model, the proposed model uses only one clock for measuring execution time of all modeled tasks.
dcterms:title
Over-approximate Model of Multitasking Application Based on Timed Automata Using Only One Clock Není k dispozici Over-approximate Model of Multitasking Application Based on Timed Automata Using Only One Clock
skos:prefLabel
Over-approximate Model of Multitasking Application Based on Timed Automata Using Only One Clock Není k dispozici Over-approximate Model of Multitasking Application Based on Timed Automata Using Only One Clock
skos:notation
RIV/68407700:21230/05:03110427!RIV06-AV0-21230___
n3:aktivita
n15:P
n3:aktivity
P(1ET400750406)
n3:dodaniDat
n9:2006
n3:domaciTvurceVysledku
n12:9687009 n12:5834805
n3:druhVysledku
n18:A
n3:duvernostUdaju
n6:S
n3:entitaPredkladatele
n8:predkladatel
n3:idSjednocenehoVysledku
535182
n3:idVysledku
RIV/68407700:21230/05:03110427
n3:jazykVysledku
n17:eng
n3:klicovaSlova
Model Checking; OSEK/VDX; Real Time; Real Time Operating System; Timed Automata; Verification
n3:klicoveSlovo
n5:Timed%20Automata n5:Real%20Time n5:OSEK%2FVDX n5:Model%20Checking n5:Verification n5:Real%20Time%20Operating%20System
n3:kodPristupu
n14:L
n3:kontrolniKodProRIV
[9DD47B0D8491]
n3:mistoVydani
Los Alamitos
n3:nosic
neuvedeno
n3:obor
n11:JC
n3:pocetDomacichTvurcuVysledku
2
n3:pocetTvurcuVysledku
2
n3:projekt
n13:1ET400750406
n3:rokUplatneniVysledku
n9:2005
n3:tvurceVysledku
Waszniowski, Libor Hanzálek, Zdeněk
n7:isbn
0-7695-2312-9
n19:organizacniJednotka
21230