About: Timed Automata Approach to Real Time Distributed System Verification     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
  • 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.
  • 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. (en)
  • 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. (cs)
Title
  • Verifikace distribuovanych systemu realneho casu casovanymi automaty. (cs)
  • Timed Automata Approach to Real Time Distributed System Verification
  • Timed Automata Approach to Real Time Distributed System Verification (en)
skos:prefLabel
  • Verifikace distribuovanych systemu realneho casu casovanymi automaty. (cs)
  • Timed Automata Approach to Real Time Distributed System Verification
  • Timed Automata Approach to Real Time Distributed System Verification (en)
skos:notation
  • RIV/68407700:21230/04:03100263!RIV08-MPO-21230___
http://linked.open.../vavai/riv/strany
  • 407;410
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • P(FD-K3/082)
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
  • 590364
http://linked.open...ai/riv/idVysledku
  • RIV/68407700:21230/04:03100263
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • Controller area network; Distributed system; Model checking; Real-Time system; Timed automata (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [8CCBBFA2FCAD]
http://linked.open...v/mistoKonaniAkce
  • Vienna
http://linked.open...i/riv/mistoVydani
  • Vienna
http://linked.open...i/riv/nazevZdroje
  • Proceedings of 2004 IEEE International Workshop on Factory Communication 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...iv/tvurceVysledku
  • Hanzálek, Zdeněk
  • Píša, Pavel
  • Waszniowski, Libor
  • Krákora, Jan
http://linked.open...vavai/riv/typAkce
http://linked.open.../riv/zahajeniAkce
number of pages
http://purl.org/ne...btex#hasPublisher
  • IEEE Industrial Electronic Society
https://schema.org/isbn
  • 0-7803-8734-1
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, 41 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software