Timed Automata Approach to Real Time Distributed System Verification
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F04%3A03100263" target="_blank" >RIV/68407700:21230/04:03100263 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Timed Automata Approach to Real Time Distributed System Verification
Original language 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.
Czech name
Verifikace distribuovanych systemu realneho casu casovanymi automaty.
Czech description
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.
Classification
Type
D - Article in proceedings
CEP classification
JD - Use of computers, robotics and its application
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/FD-K3%2F082" target="_blank" >FD-K3/082: *Advance control system designer.</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2004
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of 2004 IEEE International Workshop on Factory Communication Systems
ISBN
0-7803-8734-1
ISSN
—
e-ISSN
—
Number of pages
4
Pages from-to
407-410
Publisher name
IEEE Industrial Electronic Society
Place of publication
Vienna
Event location
Vienna
Event date
Sep 22, 2004
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—