Modellbasierte Software-Entwicklung eingebetteter Systeme

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

und

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?

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

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

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

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

Idee: Äquivalenzklassenbildung

• Partitionierung des unendlichen Zustandsraumes in endlich viele „Regionen“

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

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

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?

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

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…) ?

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

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

x>10b

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

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

x

y

Eine Region (Äquivalenzklasse)

1 2 3

1

2

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

Zonen

• 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

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

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

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

Konstruktion des Regionengraphen

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

• erfüllt die selben Sicherheitseigenschaften

x

y

Successor regions, Succ(r)

r

1 2 3

1

2

Reset region

r[y:=0]

r[x:=0]

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

Beispiel

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

(PSPACE-vollständig)

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

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