本文主要是介绍嵌入式/网络物理系统 | Timed Automata,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!
Einführung
erweitern um Uhren
- Uhren
Uhren durch x,y,z … aus C repräsentiert
nicht negative reelle Zahl
VC: Menge der Uhrenbelegung - Uhrenbedingungen Φ ( C ) \Phi(C) Φ(C)
- An Transitionen: Guards
- An Zuständen: Invarianten
Semantik
Zeitschritte ( l , v ) → ( l , v + δ ) (l,v) \rightarrow (l, v+\delta) (l,v)→(l,v+δ)
diskrete Transitionen ( l , v ) → ( l ′ , v ′ ) (l,v) \rightarrow (l',v') (l,v)→(l′,v′)
Netzwerke von Timed Automata
- Parallelkomposition
UPPAAL
Beispiel:
Aus initialzustand
x:=0 update
motion? sychronisation
Ein locationname
x == 30 Guard
x <= 30 Invariante
-
urgent und commited location
urgent: darf keine Zeit vergehen 在这个Zustand没有时间流逝
comiited: urgent + es dürfen zunächst keine Automaten weitergehen, die nicht in einer Commited Location sind. -
urgent Channels
keine Zeit-Guards -
Aufbau
globale Deklarationen
Timed Automata Templates
System Deklarationen
这篇关于嵌入式/网络物理系统 | Timed Automata的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!