嵌入式/网络物理系统 | 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)
  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

本文链接http://www.dzjqx.cn/news/show-617242.html