Original title:
Refinement of timed automata models according to hardware characteristics
Translated title:
Refinement of timed automata models according to hardware characteristics
Authors:
Hamrle, Martin ; Kofroň, Jan (referee) ; Holub, Viliam (advisor) Document type: Master’s theses
Year:
2008
Language:
eng Abstract:
[eng][cze] Timed automata have been designed for modeling a real-time system behavior over time. Main obstacle is that the formal theory assumes some unrealistic assumptions, such as that the action takes no time to execute. The model must be put more exactly, which makes the model more complicated and the whole process prone to mistakes. In the presented work we will focus on synchronization of processes over channels. There is a discussion of possible solutions. Next we will analyze chosen solutions and implement it. We will not create new tool or language but we only make extension of Uppaal language.Timed automata byla navržena na modelování real-time systémů. Formální teorie obsahuje některé nerealistické předpoklady, například nekonečně rychlé akce. Model pak musí toto chování namodelovat, což ale znepřehledňuje celý model, a tím je celé modelování náchylnější k chybám. V předložené práci se zaměříme na synchronizaci procesů pomocí kanálů. Diskutují se jednotlivé možnosti řešení zpoždění signálů. Poté následuje analýza vybraných řešení a jejich implementace. Nevytváří se nový nástroj a jazyk, ale vytváří se pouze rozšíření současného jazyka, aby bylo možné použít grafi cké prostředí nástroje Uppaal.
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/11883