嵌入式/网络物理系统

嵌入式/网络物理系统

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)

1. An Transitionen: Guards
2. 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