About: Formal Verification of Multitasking Applications Based on Timed Automata Model     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
  • Článek ukazuje jak lze pomocí časovaných automatů modelovat vícevláknové aplikace běžící pod operačním systémem reálného času kompatibilního se standardem OSEK-VDX. Uvažovaná aplikace se skládá z několika nepreemptivních úloh a obslužných rutin přerušení, které mohou být synchronizovány pomocí událostí. Nástroj pro Model-Checking je použit k verifikaci časových a logických vlastností navrženého modelu. Použití navržené metodologie je demonstrováno na automatické převodovce a výsledek verifikace nejhoršího reakčního času je je porovnán s klasickými metodami založenými na metodách time-demand analýzy. Je ukázáno, že náš přístup je méně pesimistický díky detailnějšímu modelu a úplnému prohledávání stavového prostoru (cs)
  • The aim of this paper is to show, how a multitasking application running under a real-time operating system compliant with an OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several non-preemptive tasks and interrupt service routines that can be synchronized by events. A model checking tool is used to verify time and logical properties of the proposed model. Use of this methodology is demonstrated on an automated gearbox case study and the result of the worst-case response time verification is compared with the classical method based on the time-demand analysis. It is shown that the model-checking approach provides less pessimistic results due to a more detailed model and exhaustive state-space exploration
  • The aim of this paper is to show, how a multitasking application running under a real-time operating system compliant with an OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several non-preemptive tasks and interrupt service routines that can be synchronized by events. A model checking tool is used to verify time and logical properties of the proposed model. Use of this methodology is demonstrated on an automated gearbox case study and the result of the worst-case response time verification is compared with the classical method based on the time-demand analysis. It is shown that the model-checking approach provides less pessimistic results due to a more detailed model and exhaustive state-space exploration (en)
Title
  • Formal Verification of Multitasking Applications Based on Timed Automata Model
  • Formal Verification of Multitasking Applications Based on Timed Automata Model (en)
  • Formální verifikace vícevláknových aplikací založená na časovaných automatech (cs)
skos:prefLabel
  • Formal Verification of Multitasking Applications Based on Timed Automata Model
  • Formal Verification of Multitasking Applications Based on Timed Automata Model (en)
  • Formální verifikace vícevláknových aplikací založená na časovaných automatech (cs)
skos:notation
  • RIV/68407700:21230/08:03139311!RIV09-MSM-21230___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • P(1ET400750406), P(1M0567)
http://linked.open...iv/cisloPeriodika
  • 1
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
  • 368341
http://linked.open...ai/riv/idVysledku
  • RIV/68407700:21230/08:03139311
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • Formal methods; Model-checking; Multitasking; OSEK/VDX; Timed automata; Verification (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...odStatuVydavatele
  • US - Spojené státy americké
http://linked.open...ontrolniKodProRIV
  • [B492AD570F9D]
http://linked.open...i/riv/nazevZdroje
  • Real-Time Systems
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...v/svazekPeriodika
  • 38
http://linked.open...iv/tvurceVysledku
  • Hanzálek, Zdeněk
  • Waszniowski, Libor
http://linked.open...ain/vavai/riv/wos
  • 000251900900002
issn
  • 0922-6443
number of pages
http://localhost/t...ganizacniJednotka
  • 21230
is http://linked.open...avai/riv/vysledek of
Faceted Search & Find service v1.16.116 as of Feb 22 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.3239 as of Feb 22 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 81 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software