About: Timed Automata Model of Preemptive Multitasking Applications     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)

AttributesValues
rdf:type
Description
  • Není k dispozici (cs)
  • The aim of this article is to show, how a multitasking application running under a real-time operating system compliant with the 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, model-checking theory based on timed automata and implemented in model-checking tools can be used to verify time and logical properties of the proposed model. It is shown that the proposed model is over-approximation in the case of preemptive scheduling policy. This methodology is demonstrated on automated gearbox case study.
  • The aim of this article is to show, how a multitasking application running under a real-time operating system compliant with the 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, model-checking theory based on timed automata and implemented in model-checking tools can be used to verify time and logical properties of the proposed model. It is shown that the proposed model is over-approximation in the case of preemptive scheduling policy. This methodology is demonstrated on automated gearbox case study. (en)
Title
  • Není k dispozici (cs)
  • Timed Automata Model of Preemptive Multitasking Applications
  • Timed Automata Model of Preemptive Multitasking Applications (en)
skos:prefLabel
  • Není k dispozici (cs)
  • Timed Automata Model of Preemptive Multitasking Applications
  • Timed Automata Model of Preemptive Multitasking Applications (en)
skos:notation
  • RIV/68407700:21230/05:03110425!RIV06-MSM-21230___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • P(1M0567)
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 546826
http://linked.open...ai/riv/idVysledku
  • RIV/68407700:21230/05:03110425
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • Model Checking; OSEK/VDX; Real Time; Real Time Operating System; Timed Automata; Verification (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...i/riv/kodPristupu
http://linked.open...ontrolniKodProRIV
  • [3DB010436BA9]
http://linked.open...i/riv/mistoVydani
  • Praha
http://linked.open...n/vavai/riv/nosic
  • neuvedeno
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...vavai/riv/projekt
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Hanzálek, Zdeněk
  • Waszniowski, Libor
http://localhost/t...ganizacniJednotka
  • 21230
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
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, 77 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software