Modellbasierte Software-Entwicklung eingebetteter Systeme

transcript

Prof. Dr. Holger SchlingloffInstitut für Informatik der Humboldt Universität

Fraunhofer Institut für offene Kommunikationssysteme FOKUS

Folie 2H. Schlingloff, SS2014 – modellbasierte Software-Entwicklung eingebetteter Systeme

Gibt’s hier etwa Fragen?

• Was versteht man unter Modellprüfung (Model Checking)?

• Modellierung von Echtzeit mit UML Zustandsmaschinen?

• Timed Automata?

• Semantik?

• Erweiterte Syntax?

Verifikation

• In wie weit sind zeitbeschriftete Automaten analysierbar?• Kann man entscheiden ob ein bestimmter Zustand

erreichbar ist?Excerpted from http://arpont.imag.fr/~tdang/Cours-Timed-Hyb/region-graph-ta-short.pdf

Idee: Äquivalenzklassenbildung

• Partitionierung des unendlichen Zustandsraumes in endlich viele „Regionen“

• alle Zustände einer Region weisen „ähnliches“ Verhalten auf

Quotienten

• Def. Quotientenautomat bezüglich einer Partitionierung der Zustandsmenge Abstraktion von gewissen Variablen (kleinerer

Wertebereich oder ganz weglassen) Zustände im Quotientenautomat sind

Äquivalenzklassen von Zuständen im ursprünglichen Vergröberung der Verhaltensbeschreibung: Menge

aller möglichen Abläufe (akzeptierter Wortschatz) wird größer

Gesucht: Abstraktion die die Sprache nicht vergrößert

• Bei Zeitautomaten Abstraktion der Uhrenvariablen? Reduktion des Wertebereichs der Uhren?

Sprachschatz für Zeitautomaten

• Wdh.: Jeder Pfad durch das Transitionssystem ist ein Ablauf des Automaten Def.: Pfad = ((l0, v0) –c0–>(l1, v1) –c1–>(l2, v2) –c2–

>…);l ist Ort, v ist Uhrenbelegung, c Ereignis oder Dauer

Bei Zeitschritten vi+1=vi+t,bei Kontrollschritten vi+1=vi [r:=0]

Ist diese Granularität erforderlich? z.B. (l0 –c0–>l1–c1–>l2–c2–>l3 …) ausreichend?oder (c0––>c1––>c2––>c3––>…) ?oder überhaupt nur (e0e1e2e3…) ?

Sprachschatz für Zeitautomaten

• Def. Sprache eines Automaten zeitlos: Menge aller (endlichen oder unendlichen) Wörter (ohne

Berücksichtigung Uhren) zeitabhängig: Menge von Folgen (e0 –d0–>e1–d1–>e2–d2–>e3 …) Sprache des uhrlosen Automaten enthält zeitlose Sprache

• Def. Äquivalenz von Automaten erzeugte Sprachen sind gleich zwei verschiedene Äquivalenzbegriffe zeitabhängig äquivalente Automaten sind auch zeitlos äquivalent

• Bsp. zeitlos äquivalent, aber nicht zeitabhängig äquivalent

a b ax:=0

Regionen und Zonen

•endliche Partitionierung des Zustandsraumes

Definition Regionenäquivalenz: Sei cmax die größte im Automaten vorkommende Konstante.

v R u gdw• der integrale Teil aller Uhrenbelegungen ist gleich bzw. beidesmal >cmax.• der fraktionale Teil ist beidesmal =0 oder beidesmal >0• falls x<cmax und y<cmax, dann beidesmal xy oder beidesmal yx

Eine Region (Äquivalenzklasse)

• endliche Mengen von Ungleichungen

• alle möglichen Beziehungen zwischen allen Uhrenvariablen

• Es reicht, sich auf Linearkombinationen von Variablen (c=k1*c1+…+kn*cn) zu beschränken

Definition: w Z w’ gdw

w und w’ erfüllen die selben Bedingungen der Form xi < c, xi = c, xi – xj < c, xi –xj =cwobei ccmax

Endlichkeit des Zustandsraumes

• Die Relationen haben einen endlichen Index d.h. es gibt nur endlich viele erreichbare Regionen / Zonen d.h. der Regionen/Zonengraph ist endlich

• Beweisidee (Regionen) folgt aus der Definition von R: endlich viele integrale Teile

cmax und endlich viele Vergleiche der fraktionalen Teile

• Beweisidee (Zonen) bei endlich vielen rationalen Zahlen gibt es nur endlich viele

Linearkombinationen (Summierungsmöglichkeiten), die kleiner als eine vorgegebene Schranke sind

im Automaten werden nur endlich viele Konstante erwähnt daher gibt es nur endlich viele unterschiedlich erfüllte

Bedingungen der angegebenen Art

Konstruktion des Regionengraphen

• Der Regionengraph als (endlicher) Automat ist zeitlos äquivalent zum ursprünglichen Zeitautomaten

• erfüllt die selben Sicherheitseigenschaften

Successor regions, Succ(r)

Reset region

r[y:=0]

r[x:=0]

Beispiel

• |Regionen| = |Orte| * |Konstante| * |Uhren|! • i.A. exponentiell in der Anzahl der Uhren und Konstanten

(PSPACE-vollständig)

UppAal, Kronos, Rabbit…

• Tools zur Konstruktion des Regionengraphen animierte Simulation temporale Verifikation

• unterschiedliche interne Repräsentation Mengen von Ungleichungen BDDs Differenzmatrizen, difference bound matrices

http://www.cs.auc.dk/~kgl/ARTES/sld041.htm

Modellbasierte Software-Entwicklung eingebetteter Systeme

Documents