Timed Testing - Informatik 2

Timed Testing
Christian Röller
Lehrstuhl für Software Modeling and Verification
RWTH Aachen
[email protected]
Zusammenfassung
Diese Ausarbeitung thematisiert das Testen von zeitkritischen Systemen und stellt dabei den Ansatz von Nielson und Skou [NiSk03]
in den Mittelpunkt. Die Gliedeung sieht drei Kapitel vor. Kapitel 2
beschäftigt sich mit den Grundlagen zum modellbasierten Testen, indem erst kurz auf das Testen mit Modellen allgemein eingegangen wird,
um dann die nötigen Modelle zum timed testing einzuführen. Weitergehend wird noch auf die Grundlagen für den speziellen Ansatz eingegangen, also den Hennessy Tests und der symbolic representation. Das
nächste Kapitel 3 beschreibt dann den eigentlichen Testablauf für den
Ansatz, bevor Kapitel 4 eine Zusammenfassung der Ausarbeitung gibt.
Inhaltsverzeichnis
1 Motivation
2
2 Grundlagen zur Modellierung von zeitkritischen Systemen
2.1 Model-based-testing . . . . . . . . . . . . . . . . . . . . . . . .
2.2 Hennesy Test . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3 Timed automata . . . . . . . . . . . . . . . . . . . . . . . . .
2.4 Event recording automata . . . . . . . . . . . . . . . . . . . .
2.5 Symbolic representation . . . . . . . . . . . . . . . . . . . . .
2.5.1 Timed trace Berechnung . . . . . . . . . . . . . . . . .
2.6 Zusammenfassung . . . . . . . . . . . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
3
3
4
5
7
9
11
13
3 Testen mit Hilfe des Modells
3.1 Test selection . . . . . . . . . . . . .
3.2 Zustandspartitionierung . . . . . . .
3.3 Dekorierter Äquivalenzklassengraph
3.4 Testalgorithmus . . . . . . . . . . . .
3.5 Zusammenfassung . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
15
15
16
18
19
20
4 Zusammenfassung
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
21
1
1
Motivation
Sowie die Softwareentwicklung fester Bestandteil der Informatik ist, ist auch das
Testen neuer Systeme fester nicht wegzudenkender Bestandteil der Softwareentwicklung. Testen ist in der Softwareentwicklung immer noch die dominanteste Validierungsaktivität, um ein System auf Korrektheit zu prüfen. Und trotz steigender
Komplexität in der Softwaretechnik mangelt es immer noch an leistungsstarken, automatisierten Testverfahren, sodass das Testen immernoch eine sehr zeitaufwändige
und kostenintensive Komponente einnimmt. Es besteht also ein großer Bedarf an
effektiven automatisierten Testverfahren, wobei Effektivität in diesem Kontext drei
Dinge meint. Zum einen müssen Tests effektiv hinsichtlich ihrer Ausführungszeit
sein, zum Anderen dürfen die Tests dabei nicht zuviele Resourcen des Systems
verwenden, denn diese sind schließlich begrenzt und gleichzeitig müssen effektive
Testverfahren aber auch für eine hohe Abdeckung des Test-Objekts sorgen, da eine
volle Abdeckung meist praktisch nicht umsetzbar ist.
Eine sehr vielversprechende Technik ist das modellbasierte Testen, bei der das
Verhalten des zu testenden Systems mit einem Modell dargestellt wird, um aus
diesem automatisiert Tests zu erstellen, auszuführen und auszuwerten. Es existiert
eine Vielzahl solcher modellbasierter Testansätze, wobei sich die meisten auf das
qualitative Verhalten von Software beschränken und die quantitativen Aspekte von
Software außer Acht lassen, wie zum Beispiel Echtzeiteigenschaften. Der immer
größer werdende Anteil an eingebetteten Systemen und Kommunikationssoftware, bei denen Echtzeit eine Voraussetzung zum korrekten Ablauf sind, führte zur
Erweiterung des modellbasierten Testens um den Zeitfaktor.
Dies führt uns direkt zum eigentlichen Thema dieser Arbeit, dem sogenannten timed modelbased testing oder auch kurz timed testing genannt, bei dem die
aktuellen Modelle so erweitert wurden, dass nun auch quantitative Aussagen zum
zeitlichen Ablauf der getesteten Software möglich sind. Die folgende Ausarbeitung
beschäftigt sich genau mit den angesprochenen Problemen und zeigt einen Ansatz
für modellbasiertes blackbox testing bei Systemen mit einer vorhandenen externen
Zeitbeobachtung.
2
2
Grundlagen zur Modellierung von zeitkritischen
Systemen
Dieses Kapitel beschäftigt sich mit den Grundlagen des modellbasierten Testens,
um dann aufbauend das hier verwendete Modell für timed testing einzuführen, den
sogenannten timed automata, beziehungsweise eine Spezialform dieser, den event
recording automata. Zusätzlich werden noch die zum Verständnis benötigten Hennesytests eingeführt und eine effiziente Darstellung unserer Automaten vorgestellt,
die symbolic representation, welche uns das Berechnen von timed traces ermöglicht.
2.1
Model-based-testing
Modellbasiertes Testen impliziert automatisiertes Testen. Denn es geht darum das
erwartete Verhalten der zu testenden Software in einem Modell zu spezifizieren, um
daraus automatisch Testcode ableiten zu können. Die so enstehenden Testfälle werden dann von einem speziellen Tool, welches die Testfälle interpretieren kann, auf
dem zu testenden System ausgeführt und mit den zu erwartenden Testergebnissen
verglichen. Die unten angegebene Abbildung illustriert das Verhalten nochmal ein
bischen anschauchlicher.
Abbildung 1: model-based testing
Links ist die formale Spezifikation zu erkennen, in diesem Fall ein timed automaton, welcher als Input für das Testgenerierungstool dient. Das Tool ist zum Einen
dafür verantwortlich, die Testfälle zu erzeugen, aber auch gleichzeitig eine Auswahl
dieser vorzunehmen, denn wie in den weiteren Kapiteln noch erläutert wird, lassen sich unendlich viele Testfälle aus unserem Modell ableiten. Die so erhaltene
Testsammlung wird jetzt vom Testausführungstool in eine Sprache übersetzt, die
für unsere Implementierung unter Test verständlich ist und automatisch ausgeführt
werden kann. Die sogenannte implementation relation beschreibt exakt die Konformität zwischen Spezifikation und Implementierung. Wie schon an der Abbildung zu
erkennen ist(timed automata als Modell) soll es nun aber nicht um das modellbasierte Testen von normalen Systemen gehen, sondern um das Testen von zeitkritischen
3
Systemen. Bei diesen Systemen ist nicht nur der richtige Output, sondern auch die
erwartete Zeit für diesen Output entscheident für die Korrektheit ist. Das Modell,
welches diese Zusatzeigenschaft spezifizieren soll, sind die timed automata, welche
im Kapitel 2.3 genauer erläutert werden.
2.2
Hennesy Test
Dieses Kapitel dient als Grundlage für den im Anschluss vorgestellten Ansatz von
Nielson und Skou [NiSk03], bei dem die implementation relation auf Hennessy Tests
basiert. Bei Hennessy’s Testingtheorie wird die Spezifikation mit Hilfe eines labelled
transition system mit endlichem Aktionsalphabet dargestellt. Weiter wird angenommen, dass die Implementierung durch endlich viele Beobachtungen observiert
werden kann. Die endliche Sequenz an Kommunikation zwischen Tester und Implementierung unter Test wird Berechnung genannt und im weiteren mit Comp(T k I)
bezeichnet. Jeder Ausführung eines Test wird ein Verdikt(PASS, FAIL, INCONCLUSIVE) zugeordnet. Endet eine Berechnung mit einer Beobachtung, welche dem
Verdikt PASS entspricht, so war die Berechnung erfolgreich. Grundsätzlich unterscheidet man zwischen drei Tests mit folgender Syntax:
• after σ must A
• can σ
• after σ must ∅ (cannot σ)
Dabei ist Test 1 erfolgreich, wenn mindestens eine Beobachtung aus A gemacht
wird, nachdem trace σ beobachtet wird. Test 2 ist erfolgreich, wenn σ ein Präfix
des beobachteten Systems ist und Test 3 ist erfolgreich wenn σ gerade kein Präfix
darstellt. Die Basisidee der Hennessy-Theorie ist es, zwei Systeme nur anhand ihrer Tests zu vergleichen. Somit sind zwei Systeme äquivalent, wenn ein Tester sie
nicht anhand von Tests unterscheiden kann. Da manche Berechnungen erfolgreich
ausfallen und manche nicht, lässt sich das Bestehen eines Tests nun auf zwei verschiende Varianten definieren. Entweder besteht die Implementierung den Test, wenn
eine erfolgreiche Berechnung ausreicht oder die Implementierung besteht den Test,
wenn alle Berechnungen erfolgreich ausfallen müssen. Diese beiden Varianten werden auch als may- beziehungsweise als must-preorder bezeichnet und sind wie folgt
definiert:
1. S must T gdw. ∀ Σ ∈ Comp(T k S) : Σ ist erfolgreich
2. S may T gdw. ∃ Σ ∈ Comp(T k S) : Σ ist erfolgreich
3. S vmust I gdw. ∀ T : S must T impliziert I must T
4. S vmay I gdw. ∀ T : S may T impliziert I may T
5. S vte I gdw. S vmust I und S vmay I
Bei nicht deterministischen Systemen ist zwischen diesen beiden Preorders zu
unterscheiden, denn sie sind nicht gleich ausdrucksstark. Nehmen wir dazu folgendes
Beispiel an:
Beispiel: S2 stellt zwar unter der may-preorder eine korrekte Implementierung
von S1 dar, allerdings nicht unter der must-preorder. Denn der Test after coin
must(cof ) lässt den Unterscheid der beiden Systeme erkennen. Wohingegen alle
4
coin
coin
coin
coin
cof
tea
cof
Abbildung 2: S1
coin
cof
tea
tea
Abbildung 3: S2
Abbildung 4: S3
vodka
tea
Abbildung 5: S4
Berechnungen von S1 erfolgreich ausfallen würden ist dies bei S2 nicht der Fall.
Somit stehen diese beiden Systeme nicht in der must-preorder aber wären unter
der may-preorder konform. Ein zweites Beispiel, indem ein may Test den Unterscheid erkennen lässt wäre der Fall, dass S3 keine korrekte Implementierung von S2
darstellt. Denn der Test may coin•cof lässt den Unterscheid der beiden Systeme
erkennen. Wohingegen es in S2 eine erfolgreiche Berechnung für diesen Test gibt,
ist das bei S3 nicht der Fall. Die dritte Art von Tests eignet sich um unerwünschtes
Zusatzverhalten zu testen. So ist zum Beispiel S4 keine korrekte Implementierung
von S1 , denn mit dem Test after coin•vodka must ∅(cannot coin•vodka) lassen
sich die beiden Systeme unterscheiden, insofern das S1 diesen Test immer besteht
und S4 nicht. Wichtig ist also bei der Wahl der preorder darauf zu achten ob Determinismus vorliegt oder nicht. Die hiermit vorgestellten Hennessy Tests werden im
späteren Verlauf als Grundlage der implementaion relation dienen. Mit Hilfe dieser
Test werden später sogenannte deadlock observations formuliert, die zu bestimmten
traces auftauchen müssen, möglich sein müssen oder nicht auftauchen dürfen. Um
die Hennessy Tests auch für den vorgestellten Ansatz verwenden zu können, stellen die traces im folgenden timed traces dar und die Berechnung findet auf timed
automata statt. Die Ableitung dieser timed traces wird Inhalt des Kapitels 2.5.1
sein.
2.3
Timed automata
Die timed automata erweitern die klassischen endlichen Automaten um eine endliche
Menge von Uhren über einem dichten Zeitintervall. Alle Uhren ticken dabei monoton in einer einheitlichen Rate, sodass sie die vergangene Zeit von ihrem Startpunkt
oder ihrem letzten Reset messen können. Im Gegensatz zu normalen Automaten
hängt das Schaltverhalten von timed automata nicht nur von Inputsymbolen ab,
sondern auch von den Werten der einzelnen Uhren. Jede Transition kann beliebige
Uhren des Automatens zurücksetzen und hat eventuell Schaltbedingungen, welche
sich auf die Werte der Uhren beziehen. Eine Transition ist also schaltbar, wenn
das zugehörige Inputsymbol gelesen wird und die Werte der Uhren den Zeiteinschränkungen auf der Transition entsprechen. Diese Zeiteinschränkungen haben die
folgende Syntax. Für eine Menge C von Uhren wird die Menge Φ(C) der Zeiteinschränkungen ϕ induktiv wie folgt definiert:
ϕ = c < k | c > k | c ≤ k | c ≥ k | ϕ1 ∧ ϕ2 wobei c ∈ C und k ∈ Q+
5
Ein timed automata A ist ein Tupel (S,S0 ,Σ,C,Inv,E) wobei
• S ist endliche Menge an Zuständen
• S0 ist endliche Menge an Startzuständen
• Σ ist endliches Aktionsalphabet
• C ist endliche Menge an Uhren
• Inv : S → Φ(C) ordnet jedem Zustand eine Invariante zu
• E ⊆ S × Σ × Φ(C) × 2c × S ist die Menge an Transitionen
Eine Transition (s,a,ϕ,λ,s’) beschreibt also den Übergang von Zustand s nach
s’ bei einem Symbol a ∈ Σ. Die Uhrbeschränkung ϕ ∈ Φ (guard ) beschreibt wann
eine Transition schaltbar ist und λ ⊆ C enthält die Uhren, welche beim Übergang
zurückgesetzt werden sollen. Die Zustandsinvarianten beschränken die Zeit, wielange sich der Automat in diesem Zustand befinden darf. Beispiel: Als Beispiel
soll im folgenden ein Lichtschalter dienen, welcher wie folgt als timed automaton
dargestellt werden kann.
• S = {s0 , s1 }
• S0 = {s0 }
• Σ = {on,off}
• C = {c}
• Inv(s0 ) = true, Inv(s1 ) = c ≤ 5
Das Verhalten des Automaten lässt sich wie folgt beschreiben. Der Automat
verfügt über zwei Zustände s0 , welcher den Zustand in dem das Licht aus ist repräsentieren soll und Zustand s1 , indem sich der Automat befindet wenn das Licht
an ist. Das Licht kann angeschaltet werden durch Betätigen des Knopfes on. Dies
entspricht dem Zustandswechsel von s0 nach s1 . Sollte der on Knopf nicht innerhalb
von fünf Zeiteinheiten wieder gedrückt werden, um so das Licht weiter leuchten zu
lassen, wechselt der Automat selbstständig nach genau fünf Zeiteinheiten wieder in
den Zustand s0 und löscht damit das Licht, indem er die off Aktion durchführt.
on?, c < 5, {c}
on?, true, {c}
start
s1
c≤5
s0
off!, c = 5, ∅
Abbildung 6: Beispielautomat - Lichtschalter
Dies soll als Grundlagen zu timed automata genügen, denn dieses Kapitel dient
lediglich der Einführung in das Thema. Der Hauptteil dieser Ausarbeitung wird
6
sich mit einem speziellen Ansatz zum Thema timed testing beschäftigen, bei dem
eine spezielle Variante der timed automata verwendet wird, den sogenannten event
recording automaton. Für weitere Informationen zum Thema timed automata verweise ich auf das Papier von Alur und Dill [AlDi].
2.4
Event recording automata
In diesem Abschnitt wird nun der timed automaton für den speziellen Ansatz von
Nielson und Skou [NiSk03] beschrieben, den sogenannten event recording automaton(ERA). Vorgeschlagen wurde diese spezielle Subart der timed automata von
Alur, Fix und Henzinger in [AlFH]. Formal besteht ein event recording automaton
aus folgenden Bestandteilen.
Ein ERA ist ein Tupel (Act, N, l0 , G(X), X, E), wobei
1. Act = endliche Menge von Aktionen
2. N = endliche Menge von Zuständen
3. l0 = Startzustand
4. G(X) = Menge von Guards (Uhrbeschränkungen)
5. X = Menge der Uhren = {xa | a ∈ Act}
6. E ⊆ N × G(X) × Act × N = Menge der Transitionen
ist. Genauso wie ein timed automaton, besitzt also auch ein ERA eine endliche
Menge an Uhren, wobei jede Uhr genau einer Aktion zugeordnet ist, die sogenannte eventclock. Diese Uhr misst die Zeit zwischen dem aktuellen und dem letzten
Auftreten dieser Aktion, denn sie wird automatisch bei der Ausführung ihrer Aktion zurückgesetzt. Keine weiteren Uhren dürfen zurückgesetzt werden. Des Weiteren
sind keine τ Transitionen erlaubt und auch nur ein Startzustand ist gestattet. Diese
Einschränkungen führen zur Determinierbarkeit von ERAs. Als Letztes wird noch
angenommen, dass alle Aktionen sofort umgesetzt werden und keine Synchronisierung mit der Umwelt nötig ist. Ohne diese Annahme könnte man keine Aussagen
treffen, ob die Zeitgrenzen eingehalten wurden, da man nicht weiß, wie lange die
Synchronisation gedauert hat. Das folgende Beispiel soll dem besseren Verständnis
beitragen.
7
start
s1
coin?
s2
give?, xcoin≥2 ∧ xcoin≤4
give?, xcoin≥4
s3
s4
cof!, xgive≥2
thincof!, xgive≥1
s5
s6
Abbildung 7: Beispiel ERA Kaffeeautomat(n. det.)
Beispiel: Der oben abgebildete Kaffeeautomat hat die besondere Funktion das
er auf die Schnelligkeit seiner Benutzer reagiert und dementsprechend dünnen beziehungsweise normalen Kaffee brüht und ist im Detail wie folgt zu verstehen. Der
Benutzer startet mit dem Einwurf einer Münze(coin? ), wodurch die eventclock für
coin zurückgesetzt wird. Im Zustand s2 muss der Benutzer den Knopf give(give? )
betätigen. Je nachdem in welcher Zeit dies geschieht, wechselt der Automat in
Zustand s3 (bei größergleich vier Zeiteinheiten) oder in s4 (bei einer Zeiteinheit zwischen zwei und vier) und erhält somit entweder dünnen oder normalen Kaffee.
Schnell zu erkennen ist, dass dieser Automat nicht deterministisch ist, denn es ist
unklar wie sich der Automat verhält, wenn der Benutzer nach genau vier Zeiteinheiten den give Knopf betätigt, denn dann sind laut Spezifikation normaler sowie
auch dünner Kaffee möglich. Wie schon anfangs erwähnt, lassen sich ERAs aber
determinieren. Die genaue Prozedur ist in [AlFH] nachzulesen und ist der Potenzmengenkonstruktion von normalen Automaten sehr ähnlich. Das folgende Beispiel
soll die Prozedur illustrieren.
8
start
s1
coin?
s2
give?, xcoin≥2 ∧ xcoin<4
give?, xcoin>4
give?
xcoin=4
s3,4
s3
s4
thincof!
xgive≥1
cof!
xgive≥2
cof!, xgive≥2
thincof!, xgive≥1
s5
s6
Abbildung 8: Beispiel ERA Kaffeeautomat(det.)
Beispiel: Wie man sieht entsteht also ein neuer Zustand s3,4 , zusammengesetzt
aus s3 und s4 , welcher alle ausgehenden Transitionen seiner Teilzustände erhält.
Sodass nun von Zustand s2 nur noch eine deterministische Wahl der Transitionen möglich ist. Semantisch gesehen ist ein timed automata ein labelled transition
system mit unendlichen vielen Zuständen aufgrund des dichten Zeitintervalls. Es
benötigt also einer Technik, die diese Unendlichkeit auf eine endliche Art und Weise
ausdrücken kann und effizient Berechnungen darauf anstellen kann. Daher wird nun
im folgenden Kapitel 2.5 eine symbolische Repräsentation der Zustände eingeführt.
2.5
Symbolic representation
Wie schon im Kapitel zuvor erwähnt lassen sich timed automata nicht mit endlichen
Zustandstechniken, die alle konkreten Zustände betrachten, analysieren. Daher verwendet der hier vorgestellte Ansatz eine symbolische Repräsentation. Ein Zustand
in einem Automaten kann als Paar (l, u) verstanden werden, wobei l dem aktuellen
Zustand des Automatens entspricht und u dem Vektor der aktuellen Uhrenwerte. Da es von diesen Zuständen unendlich viele gibt, wird der Begriff der zone
eingeführt. Wobei eine zone eine Konjunktion von Uhrbeschränkungen und Uhrdifferenzen darstellt, oder anders gesagt die Lösungsmenge der zulässigen Uhrenwerte
darstellt.
9
Ein symbolischer Zustand [l,z] repräsentiert also eine unendliche Menge an Automatenzuständen der Form {( l, u ) | u ∈ z }. Zones können mithilfe von difference
bound matrices dargestellt und effizient manipuliert werden, das genaue Vorgehen
wird von Dill in [Dill89] formuliert. Das Aussehen und die Nützlichkeit von zones
soll das folgende Beispiel illustrieren.
start
start
[s1 ,z]
z=Xcoin ∈ [0,∞) ∧
Xgive ∈ [0,∞) ∧
Xcoin − Xgive = 0
coin?
s1
[s2 ,z]
z=Xcoin = 0 ∧
Xgive ∈ [0,∞) ∧
Xgive − Xcoin ∈ [0,∞)
coin?
s2
give?, Xcoin ∈ [2,4)
give?, Xcoin ∈ [2,4)
s4
[s4 ,z]
z=Xcoin ∈ [2,4) ∧
Xgive = 0 ∧
Xcoin − Xgive ∈ [2,4)
thincof!, Xgive ∈ [1,∞)
s6
thincof!, Xgive ∈ [1,∞)
[s6 ,z]
z=Xcoin ∈ [3,∞) ∧
Xgive ∈ [1,∞) ∧
Xcoin − Xgive ∈ [2,4)
Abbildung 9: Ausschnitt aus Kaffeemaschinenautomat und zugehörige symbolische Zustände
Beispiel: Die obige Abbildung beschreibt zwei Dinge. Auf der linken Seite ist ein
Ausschnitt des zuvor abgebildeten deterministischen Kaffeeautomatens zu erkennen
und zwar der rechte Teil bei dem der Benutzer sich für einen dünnen Kaffee entschieden hat. Auf der rechten Seite sind die zugehörigen symbolischen Zustände zu
erkennen. Man erkennt an diesen Zuständen die Intervalle beziehungsweise Werte
der Uhren, die sie beim Eintritt zu erfüllen haben und die Differenzen der einzelnen
Uhren. Man erhält den nächsten Zustand indem man Zeit entsprechend der guards
10
auf den Transitionen vergehen lässt. So sieht man zum Beispiel am symbolischen
Zustand [s4 ,z], dass die Xcoin -Uhr beim Eintritt im Intervall [2,4) liegen muss und
die Xgive -Uhr beim Eintritt zurückgesetzt wurde. Die Differenz entspricht somit
dem Wert von der Xcoin -Uhr. Wenn man nun Zeit entsprechend des guards an der
Transition vergehen lässt, also mindestens eine Zeiteinheit, dann erhält man die
zone für Zustand [s6 ,z]. Hierbei ändert sich die Differenz nicht, da weder die Xcoin
noch die Xgive -Uhr zurückgesetzt wurde. Die symbolische Repräsentation liefern
also eine Möglichkeit den unendlichen Zustandsraum eines timed automata auf eine
endliche Weise darzustellen und darauf effizient Erreichbarkeitsberechnungen anstellen zu können. Desweiteren ist es nun auch möglich, mithilfe der symbolischen
Zustände, timed traces im Automaten zu berechnen. Was dabei zu beachten ist und
wie die Berechnung aussieht wird exemplarisch im Abschnitt 2.5.1 erläutert.
2.5.1
Timed trace Berechnung
Dieser Abschnitt gibt eine exemplarische Beschreibung der Ableitung von timed
traces, welche als Grundlage für die Hennessy Tests dienen werden, mit dessen Hilfe die deadlock-observations formuliert werden sollen. Das genaue Vorgehen wird
in Kapitel 3 beschrieben, hier soll es nun erstmal nur um die Ableitung gehen. Zur
Berechnung werden, wie schon erwähnt, die im Kapitel zuvor vorgestellten symbolisches Zustände verwendet. Ist ein symbolischer Zustand erreichbar so impliziert das,
dass auch alle von ihm repäsentierten konkreten Zustände erreichbar sind, allerdings
ist bei der Berechnung des timed traces zu diesem Zustand zu beachten, dass nicht
alle konkreten Zustände auf diesem Pfad zum gewünschten ausgewählten konkreten
Zustand führen, sondern nur eine Teilmenge. Die Wahl eines konkreten Zustands
beeinflusst also die Wahl der Zustände auf dessen Pfad. Grundsätzlich läuft die
Berechnung eines timed traces wie folgt ab. Von dem ausgewählten symbolischen
Zustand, bei dem der Pfad enden soll, wählt man einen konkreten Zustand, dass
heißt man wählt konkrete Uhrenwerte, welche in diesem Zustand gelten können.
Nun errechnet man die Zustände auf dessen Pfad durch back-propagation und Einbeziehung der einzelnen guards auf den gewählten Transitionen, indem man auch
konkrete Werte für diese Zustände wählt, wobei hier natürlich die anfangs erwähnte
Problematik zu beachten ist. Das folgende Beispiel soll diesen Prozeß ein wenig genauer beschreiben.
Beispiel: Das Beispiel ist wie folgt zu verstehen. Auf der rechten Seite der
Abbildung 10 sind die symbolischen Zustände aus dem Beispiel zuvor wieder zu
erkennen, welche benutzt werden sollen um einen can σ • thincof Hennessytest zu
generieren. Da eine korrekte Implementierung in diesem Zustand, bei korrekter
Wahl der Uhrenwerte, dünnen Kaffee produzieren können muss. Und genau um
die Berechnung dieses korrekten Pfads geht es in diesem Beispiel. So sind auf
der linken Seite die konkret gewählten Zustände zu erkennen, welche ein Beispiel
für genau so einen Pfad darstellen. Angefangen in Zustand s4 musste so für die
eventclock (EC) von Xgive ein Wert im Intervall [1,∞) gewählt werden damit der
guard der thincof ! -Transition erfüllt ist. Hier wurde der Wert zwei gewählt. Diese
Wahl beeinflusste aber indirekt die Wahl von der EC von Xcoin in diesem Zustand,
denn die Differenz der beiden Uhren muss im Intervall [2,4) liegen. Somit ist der
Wert nun auf das Intervall [4,6) beschränkt. Hier wurde der Wert fünf gewählt. Die
Wahl dieser beiden Werte beeinflusst aber auch die Wahl der Werte im Zustand
davor. Denn die Tatsache das im Zustand s4 zwei Zeiteinheiten verblieben wird,
11
start
start
s1
Xcoin = 1
Xgive = 1
[s1 ,z]
z=Xcoin ∈ [0,∞) ∧
Xgive ∈ [0,∞) ∧
Xcoin − Xgive = 0
coin?
[s2 ,z]
z=Xcoin = 0 ∧
Xgive ∈ [0,∞) ∧
Xgive − Xcoin ∈ [0,∞)
coin?
s2
Xcoin = 3
Xgive ∈ [3,∞) = 4
give?, Xcoin ∈ [2,4)
give?, Xcoin ∈ [2,4)
s4
Xcoin ∈ [4,6) = 5
Xgive ∈ [1,∞) = 2
[s4 ,z]
z=Xcoin ∈ [2,4) ∧
Xgive = 0 ∧
Xcoin − Xgive ∈ [2,4)
thincof!, Xgive ∈ [1,∞)
can σ • thincof
Abbildung 10: Timed trace Berechnung Beispiel
da die EC Xgive gleich zwei ist und die EC von Xcoin beim Übergang von s2
nach s4 nicht zurückgesetzt wurde legt indirekt fest, dass der Wert von der EC
für Xcoin im Zustand s2 gleich drei sein muss. Da sonst der Wert von fünf im
Zustand s4 durch Verbleiben von zwei Zeiteinheiten nicht möglich gewesen wäre.
Durch die Festlegung des Wertes auf drei wird auch wieder indirekt das Intervall
von der EC für Xgive im Zustand s2 auf das Intervall [3,∞) eingeschränkt, denn
der Wert muss mindestens dem Wert von der EC für Xcoin entsprechen, denn
diese wurde beim Übergang in den Zustand zurückgesetzt. Hier wurde sich für
den Wert vier entschieden. Natürlich beeinflusst auch die Wahl dieses Wertes die
Wahl der beiden Werte im Zustand davor, beziehungsweise schränkt sie diesmal
sogar auf genaue Werte ein. Denn durch die Tatsache, dass im Zustand s2 nun
drei Zeiteinheiten verbracht werden soll, da die EC für Xcoin den Wert drei hat,
muss auch im Zustand s1 eine Zeiteinheit verbracht werden, da sonst nicht der
Wert vier von der EC von Xgive im Zustand s2 erreicht werden kann. Da diese
Uhr beim Übergang von s1 nach s2 nicht zurückgesetzt wird. Da die Differenz im
Zustand s1 null betragen muss, nehmen beide Uhren den Wert eins an. Der genaue
timed trace für den can-Test sieht also wie folgt aus, can 1coin3give2thincof .
Semantisch ist dieser Test wie folgt zu verstehen. Warte eine Zeiteinheit, führe die
Aktion coin aus, warte wieder drei Zeiteinheiten, führe Aktion give aus, warte zwei
12
Zeiteinheiten, dann erfolgt der Output thincof. In einer korrekten Implementierung
muss es eine erfolgreiche Berechnung für diesen Test geben. Die Wartezeiten sind
an den Uhren, die zuvor zurückgesetzt wurden, abzulesen. Zu erkennen ist also,
dass die Wahl der delays völlig beliebig ist solange sie den guards, beziehungsweise
den daraus resultierenden Intervallen genügen. Eine begründete Frage ist also: Wie
soll die Wahl der delays aussehen? Da es natürlich nicht möglich ist alle Werte der
Intervalle zu testen wählt man in der Praxis meist die folgenden.
1. Ein delay an der unteren Schranke des Intervalls, um die Unverzüglichkeit
(promptness) des Systems zu testen.
2. Ein delay in der Mitte des Intervalls, um die Beständigkeit(persistence) des
Systems zu testen.
3. Ein delay an der oberen Schranke des Intervalls, um die Ausdauer(patience)
des Systems zu testen.
Auch wenn vielleicht die untere Schranke das wichtigste delay eines Tests darstellt, um deadline-errors zu erkennen, so kann es durchaus auch wichtig sein die
obere Schranke zu testen, um eventuell frühzeitig abgelaufene timer zu erkennen.
2.6
Zusammenfassung
In diesem Kapitel wurde zunächst das Thema model-based testing(MBT) ganz allgemein eingeführt und auf die einzelnen Konponenten Bezug genommen. So ist klar
geworden, dass es beim MBT um die automatische Testgenerierung aus einem Modell geht, welches das eigentlich zu testende System spezifiziert. Weitere Aufgaben
eines solchen test frameworks sind neben der eigentlichen Ableitung der Testfälle
auch die Auswahl und Ausführung geeigneter Test, denn oft existieren unendlich
viele Tests. Gerade beim timed testing ist dies aufgrund des dichten Zeitintervalls
immer der Fall. Bei der Ausführung muss natürlich auch ein Tool existieren, welches
die abstrakten Tests in eine für die implementation under test verständliche Sprache
bringt und die Tests auswertet. Im Weiteren ging es dann nurnoch um das modellbasierte timed testing und es wurde das Modell der timed automata vorgestellt.
Diese Automaten stellen eine Erweiterung der normalen endlichen Automaten dar,
indem auch noch eine endliche Menge an Uhren zum Modell gehören, welche die
relative Zeit zwischen dem aktuellen und dem zuletzt aufgetreten Symbol messen
können. Besondere Merkmale dieser Automaten, wie zum Beispiel die nicht allgemein geltende Determinierbarkeit wurden in dieser Ausarbeitung nicht behandelt
und nur auf das Papier von Alur und Dill [AlDi] verwiesen. Im nächsten Unterkapitel wurden dann die Hennessy Tests beschrieben, denn auf Diesen basiert die
implementation relation des ERA-Ansatz von Nielson und Skou [NiSk03]. Mit Hilfe
dieser Tests werden die nötigen deadlock-observations beschrieben, welche im Kapitel 3 genauer beschrieben werden. Basisidee der Hennessy Theorie ist es, Systeme
nur anhand von Tests zu unterscheiden. Hierbei ist aber darauf zu achten ob es sich
um deterministische Systeme handelt oder nicht, wie es im Beispiel gezeigt wurde.
Der nächste Abschnitt beschäftigte sich mit dem eigentlich Modell des Ansatzes,
den sogenannten event recording automata. Diese stellen eine determinierbare Subklasse der timed automata dar. Die Determinierbarkeit wird durch das Einführen
von eventclocks und dem Verbieten von τ Transitionen erreicht. Ein großes Problem
beim Ableiten von Tests von einem timed automata(TA) ist die Tatsache, dass jeder TA über einen unendlichen Zustandsraum verfügt, welchen es in den Griff zu
13
bekommen gilt. Die hierfür eingeführte Variante der symbolischen Zustände löst
das über sogenannte zones, welche eine unendlich Menge an konkreten Automatenzuständen repräsentieren kann. Somit wurde eine endliche Darstellung geschaffen
mit der auch über die sogenannten difference bound matrices effiziente Berechnungen zum erreichbaren Zustandsraum und der timed traces angestellt werden kann.
Genauer wurde dieses Verfahren im Papier von Dill [Dill89] beschrieben. Im letzten Teil dieses Kapitels wurde dann nochmal exemplarisch auf die Berechnung der
timed traces eingegangen um auf die Schwierigkeiten hinzuweisen. Zusammenfassend hat dieses Kapitel die Grundlage zum Spezifizieren und Ableiten der Testfälle
geliefert, im nächsten Kapitel muss jetzt noch der Fragestellung nachgegangen werden, wie die Tests auf eine endliche Menge selektiert werden. Und wie die Tests im
allgemeinen, also auch die schon mehrfach angesprochenen deadlock-observations,
genau aussehen.
14
3
Testen mit Hilfe des Modells
Dieses Kapitel behandelt das wichtige Thema der Testselektion, denn das Abdecken
aller Testfälle ist beim timed testing aufgrund der Zeitkomponente nicht möglich. In
dem vorgestellten Ansatz wird das über einen sogenannten Äquivalenzklassengraphen
gelöst, welcher Zustände des Automatens anhand von Uhreinschränkungen zusammenfasst und gefordert wird, dass für jede dieser Äquivalenzklassen mindestens ein
Test durchgeführt wird. Des weiteren wird auch noch die Einführung von deadlockobservations mit Hilfe der Hennessy Tests thematisiert um die Korrektheit des getesteten Systems zu gewährleisten. Am Ende des Kapitels wird noch der Algorithmus vorgestellt, welcher das Zusammenspiel aller kennengelernten Komponenten
beschreibt.
3.1
Test selection
Wie schon oft zuvor erwähnt, ist gründliches Testen, also das Abdecken aller Testfälle,
praktisch nicht durchführbar, denn es existieren meist schon bei normalen Systemen, durch zum Beispiel Schleifen im Programmcode, unendlich viele dieser
Testfälle. Beim timed testing wird dies durch die Zeitkomponente noch erschwert, da
hier durch das dichte Zeitintervall immer unendlich viele Testfälle existieren. Um
praktisch Testen zu können ist also eine Selektion von Testfällen unumgänglich.
Grundsätzlich beschreibt eine solche Selektion eine endliche Menge an relevanten Vertretern für die unendliche Zustandsmenge. Was im konkreten Fall für Relevant gehalten wird hängt ganz speziell vom gewählten selection criterion ab,
denn dieses beschreibt welche Tests gewählt werden sollen um die coverage zu
maximieren. Coverage, Selektion und praktische Ausführbarkeit stehen also im
ständigen Konflikt, so führt eine detailliertere Selektion zwar zu einem höheren
coverage-Maß, allerdings wächst die Testsammlung dadurch auch an, was sich negativ auf die Ausführungszeit auswirkt. Ein Kompromiss ist also aus praktischen
Ausführungsgründen nicht zu vermeiden. Die in Kapitel 2.2 vorgestellte implementation relation basierend auf den Hennessy Tests beschreibt welche Tests generiert werden sollen. Allerdings ist auch die Einschränkung, dass nur Hennessy
Tests, welche von der Spezifikation erfüllt werden auch erzeugt werden nicht genug, denn damit ist das Problem der unendlichen Testfälle noch nicht gelöst. Daher wird für diesen Ansatz ein selection criterion gewählt, welches den Zustandsraum des Automatens in grobe Äquivalenzklassen einteilt. Die Partitionierung wird
anhand der möglichen Uhrenwerte in den einzelnen Zuständen vorgenommen. Es
wird also insgeheim angenommen das sich jeder Zustand aus solch einer Klasse
äquivalent verhält und man somit nicht jeden einzelnen konkreten Zustand testen muss. Zusätzlich wird jede Äquivalenzklasse mit allen benötigten deadlockobervations dekoriert und gefordert, dass für jede Observation jeder Klasse mindestens ein Test generiert wird um Korrektheit zu gewähren so wie es die testing
preorder aus Kapitel 2.2 vorschreibt. In der Literatur wurde dieses Kriterium stable
edge set criterion benannt, da die Spezifikation stabil hinsichtlich der beobachteten
Zustände bleibt. Nur die Uhrenwerte sind entscheident für den Übergang in die
einzelnen Zustände. Es kann also angenommen werden, dass auch die Implementierung stabil ist, denn es müssen keine weiteren Aktionen ausgeführt werden um
das Verhalten der Spezifikation zu gewährleisten. Wenn die Implementierung also
unerwartet den Zustand ändert, muss dafür ein internes Signal verantwortlich sein
und das Verhalten sollte somit noch einmal überprüft werden. Das folgende Beispiel
15
beschreibt das Aussehen und die Bildung der Äquivalenzklassen.
[s3,4 , p5 ]
p5: Xgive ≥2
cannot coin
cannot give
can cof
can thincof
must{cof,thincof}
[s3,4 , p6 ]
p6: Xgive ∈[1,2)
[s3,4 , p7 ]
p6: Xgive <1
cannot coin
cannot give
cannot cof
can thincof
cannot
cannot
cannot
cannot
coin
give
cof
thincof
Abbildung 11: Äquivalenzklassen für Zustand s3,4
Beispiel Das obige Beispiel zeigt die Äquivalenzklassen für den Zustand s3,4
aus dem deterministischen Kaffeeautomaten aus Kapitel 2.4. Für diesen Zustand
wurden die entscheidenen Uhrenwerte für die eventclock von Xgive in drei Domänen
partitioniert. Zum einen die Domäne Xgive ≥ 2, bei der beide Transitionen erfüllt
sind, zum anderen Xgive ∈[1,2), bei der nur die thincof Transition erfüllt ist und
zuletzt Xgive < 1 bei der keine Transition erfüllt ist. Jede Klasse wird mit den
angesprochenen deadlock-observations dekoriert, so muss es beispielsweise in der
Äquivalenzklasse [s3,4 , p5 ] möglich sein sowohl Kaffee als auch dünnen Kaffee erhalten zu können. Weiter noch muss sogar eine der beiden Beobachtungen bei jeder Berechnung gemacht werden und der Einwurf von einer Münze beziehungsweise das Drücken der give Taste muss in diesem Zustand verboten sein. Das
nächste Kapitel beschreibt den genauen Algorithmus zur Erzeugung eines solchen
Äquivalenzklassengraphs und zeigt den vollständigen Graphen für das Beispiel des
Kaffeeautomatens.
3.2
Zustandspartitionierung
Dieses Kapitel soll den Algorithmus zur Partitionierung des Zustandsraums und Erzeugung des Äquivalenzklassengraphs beschreiben. Eine Äquivalenzklasse wird repräsentiert von einem Paar [S’,p], wobei S’ die Menge der Zustandsvektoren enthält
und p ist die Ungleichung, welche die Uhreneinschränkungen bescheibt, die in dieser
Klasse gelten muss. Um die Wiederverwendung der symbolischen Repräsentaion zu
gewährleisten, werden die Einschränkungen in disjunktive Normalform gebracht.
Hierzu einige Notationen. Zustandspartitionierung Ψ(S’)
• S’ = Menge der Zustandsverktoren
• E(S’) = Menge der Transitionen von einem Zustand aus S’
−→
• τ (E) = Menge der Guards von E = {ϕ ∈ Φ(C) | s −
ϕ,
a s0 ∈ E}
• P = Beschränkung über die Uhrungleichungen γ
W V
• DNF(P) = P in disjunktiver Normalform i j γij = P
Jedes Disjunkt in disjunktiver Normalform kann als guard ϕ ∈ Φ(C) geschrieben werden. Die DNF kann somit als Disjunktion über den guards interpretiert
16
werden, sodass
W
i
ϕi =
W V
i
j
γij .
V
V
0
Lasse Ψ(S 0 ) = {PE 0 | E 0 ∈ 2E(S ) ∧ PE 0 = ϕ∈τ (E 0 ) ϕ ∧ ϕ∈τ (E(S 0 )−E 0 ) ¬ϕ},
dann ist GDNF die Menge an guards ϕi , dessen Disjunktion der DNF entspricht.
GDNF(PE 0 ) = {ϕi ∈ Φ(C) |
W
i
ϕi = DN F (PE 0 )}
und schließlich ist
ΨDN F (S 0 ) =
S
PE 0 ∈Ψ(S 0 )
GDN F (PE 0 ).
Beispiel Als Beispiel soll hier der Zustand s3,4 aus dem deterministischen Kaffeeautomaten dienen, für den schon die Äquivalenzklassen in Kapitel 3.1 ohne Algorithmus bestimmt wurden.
Somit ist S’ = {s3,4 } und die Transitionen von S’ lauten
E(S’) = {(s3,4 , cof !, Xgive ≥ 2, s5 ), (s3,4 , thincof !, Xgive ≥ 1, s6 )},
die guards von S’ sind
τ (E(S 0 )) = {Xgive ≥ 2, Xgive ≥ 1}
Zur Vereinfachung betrachten wir 2τ (E(S
2τ (E(S
0
))
0
))
anstatt 2E(S
0
)
= {∅, {Xgive ≥ 2, Xgive ≥ 1}, {Xgive ≥ 2}, {Xgive ≥ 1}} und
Ψ(S 0 ) = {(Xgive < 2) ∧ (Xgive < 1), (Xgive ≥ 2) ∧ (Xgive ≥ 1),
(Xgive ≥ 2) ∧ (Xgive < 1), (Xgive ≥ 1) ∧ (Xgive < 2)}
Die DNF von Ψ(S 0 ) lautet
ΨDN F (S 0 ) = {Xgive < 1, Xgive ≥ 2, ∅, Xgive ∈ [1, 2)}
Damit lauten die Äquivalenzklassen genau wie in Kapitel 3.1
[s3,4 , Xgive < 1], [s3,4 , Xgive ≥ 2] und [s3,4 , Xgive ∈ [1, 2)]
17
Abbildung 12: vollständiger Äquivalenzklassengraph
Die obige Abbildung zeigt nochmal den vollständigen Äquivalenzklassengraph
für das deterministische Kaffeeautomatenbeispiel aus Kapitel 2.4. Die oberen drei
Klassen in der dritten Spalte von links stellen genau die zuvor algorithmisch erstellten Klassen dar. Kapitel 3.3 beschreibt nochmal genauer das Dekorieren des
Äquivalenzklassengraphen, also das Finden der richtigen Deadlock-Observations.
3.3
Dekorierter Äquivalenzklassengraph
Um die Mengen an Aktionen für die einzelnen Tests(must, may, cannot) zu finden
berechnet der Algorithmus folgende Mengen.
−
Sort([L,p]) = {a | ∃(L, u) ∈ [L, p] : (L, u)→
a } und
Must([L,p]) = {A | ∃(L, u) ∈ [L, p] : (L, u) |= after must A}
Damit sehen die Mengen für die einzelnen Tests wie folgt aus:
• M([L,p]) = Must([L,p]).
• C([L,p]) = Sort([L,p]).
• R([L,p]) = Act - Sort([L,p]).
M enthält also alle nötigen Mengen um die must-Tests zu generieren, C für
die may-Tests und R für die refusal -Tests(cannot-Test). Wenn also σ ein Pfad zur
Klasse [L,p] darstellt und A ∈ M ([L, p]) dann ist after σ must A ein Test, welcher
für die Klasse bestanden werden muss. Analog sind can σ • a und after σ • a must
∅(cannot σ • a) Tests, falls a ∈ C([L, p]) beziehungsweise a ∈ R([L, p]).
18
3.4
Testalgorithmus
Dieses Kapitel soll näher beschreiben, wie die Testableitung mittels der symbolischen Repräsentation aus Kapitel 2.5 und die Testselektion über den Äquivalenzklassengraphen
aus dem vorherigen Kapitel 3.2 in Kombination genutzt werden um zulässige Tests
zu generieren. Zulässig meint hier, dass nur die Tests abgeleitet werden, welche von
der Spezifikation erfüllt werden, um soundness zu gewährleisten. Denn die Konstruktion des Äquivalenzklassengraphs beinhaltet zwar alle nötigen Informationen
zum Generieren der Hennessy Tests, allerdings darüber hinaus auch noch Informationen die nicht in der Spezifikation auftauchen. Ein so abgeleiteter Test könnte also
unsound sein, im Sinne, dass das Resultat des Tests als nicht bestanden ausfällt,
obwohl die Implementierung konform zur Spezifikation ist. Um also wirklich nur die
Hennessy Tests zu erzeugen, welche von der Spezifikation erfüllt werden und somit
soundness zu garantieren wird die symbolische Repräsentation genutzt, welche nur
die erreichbaren Zustände in Betracht zieht. Zum Beispiel darf es keinen Test für
Zustand s3,4 geben bei dem die Uhren für Xcoin und Xgive jeweils den Wert zwei
haben, denn immer wenn Zustand s3,4 beobachtet wird ist der Wert für Xcoin mindestens vier. (siehe Besipiel aus Kapitel 2.4)
Der Gesamtalgorithmus zur Erzeugung und Selektion der relevanten Tests sieht
also wie folgt aus:
1. Berechne Sp = Äquivalenzklassengraph.
2. Berechne Sr = symbolic reachabilty graph von Sp .
3. Dekoriere jedes Zustand [L,z/p] ∈ Sr mit den Mengen M,C,R.
4. Tested := ∅
5. Sr durchlaufen. f orall[L, z/p] ∈ Sr : if 6 ∃ z’ : [L,z’/p] ∈ Tested then
Tested := Tested ∪ {[L,z/p]} und berechne Tests
(1) wähle (l, u ∈) [L,z/p]
(2) berechne konkreten Pfad von (l0 , 0) zu (l, u)
(3) erzeuge Testfälle:
if A ∈ M([L,p]) then after σ must A ist relevanter Test
if a ∈ C([L,p]) then can σ • a ist relevanter Test
if a ∈ R([L,p]) then after σ • a must ∅ ist relevanter Test
Der oben aufgeführte Algorithmus ist wie folgt zu verstehen. Schritt eins erzeugt den Äquivalenzklassengraph wie beschrieben in Kapitel 3.2. Schritt zwei erzeugt den symbolic reachability graph, exemplarisch beschrieben in Kapitel 2.5. Ein
symbolischer Zustand [L,z/p] in diesem Graph charakterisiert die Menge an erreichbaren Uhrenwerten, welche auch für p gelten. Eine Kante in diesem Graph drückt
aus, dass der Zielzustand erreichbar ist durch Ausführung einer Aktion a und dem
Warten einer bestimmten Zeit. In Schritt drei werden diese Zustände mit den in
Kapitel 3.3 angesprochenen Mengen an Aktionen für die einzelnen Hennessy Tests
dekoriert. Und Schritt fünf stellt den eigentlich Testgenerierungsschritt anhand dieser Mengen dar. Bei der Berechnung der timed traces in Schritt fünf gilt es natürlich
clevere Delays zu wählen so wie zum Beispiel beschrieben in Kapitel 2.5.1. Also zum
Beispiel die unteren und oberen Schranken der Intervalle zu testen, da diese wohl
die wichtigsten Tests für die Unverzüglichkeit und Ausdauer des Systems in der
Praxis darstellen.
19
3.5
Zusammenfassung
In diesem Kapitel ging es um die Testselektion beim timed testing, welche bei dieser Art des Testens einen ganz besonderen Stellenwert einnimmt, denn auch wenn
vollständiges Testen schon bei normalen Systemen meist nicht möglich ist, so hat
man beim timed testing immer das Problem der unendlichen Testfälle. Und da
theoretisch grundsätzlich jeder Test gleich wichtig ist, gilt es eine Selektion zu
finden, die den Zustandsraum in eine möglichst sinnvolle Partitionierung bringt,
sodass davon auszugehen ist, dass sich jeder konkrete Zustand in dieser Partition äquivalent verhält. In dem hier konkret gewählten Ansatz wird diese Partitionierung durch einen Äquivalenzklassengraph 3.2 vorgenommen, welcher für jeden
Zustand des Automatens Äquivalenzklassen erzeugt. Grundlage für die Erzeugung
sind die guards auf den ausgehenden Transitionen jedes Zustandes, sodass die Uhrenwerte in sogenannte Domänen eingeteilt werden, dass entweder keine Transition
schaltbar ist(Refusalzustand, sofern Konjunktion der guards keine Tautologie darstellt), jede Transition einzeln schaltbar ist(soweit möglich wenn sich guards nicht
überschneiden) und alle Transitionen gleichzeitig schaltbar(sofern möglich wenn
sich guards nicht gegenseitig ausschließen) sind. Jede so erzeugte Klasse wird mit
den beschriebenen deadlock-observations dekoriert 3.3, welche den in Kapitel 2.2
eingeführten Hennessy Tests entsprechen. Diese Observationen sollen das mögliche,
erwartete und nicht mögliche Verhalten der Zustände, welche von diesen Klassen
repräsentiert werden, definieren. Der letzte Abschnitt dieses Kapitels hat den Gesamtalgorithmus für die Testgenerierung beschrieben, also das Zusammenspiel zwischen der symbolischen Repräsentation, zum Berechnen der timed traces und dem
erreichbaren Zustandsraum, und dem Äquivalenzklassengraph zur Testselektion.
20
4
Zusammenfassung
Zunächst wurde kurz das Thema des modellbasierten Testens beschrieben, wobei es
darum geht das erwartete Verhalten einer Implementierung anhand eines Modells
zu spezifizieren, um aus diesem Modell automatisch Testfälle ableiten und selektieren zu können. Das Modell beim timed testing sind die timed automata, welche
die endlichen Automaten um eine endliche Menge an Uhren erweitern um somit
auch die Zeit zwischen den einzelnen Aktionen messen zu können. Ein weiteres
gundlegendes Thema waren die Hennessy Tests, welche im weiteren Verlauf des
beschriebenen Ansatzes die Grundlage für die zu testenden deadlock-observations
darstellten. Basisidee der Hennessytheorie ist es zwei Systeme nur anhand ihrer Test
zu unterscheiden. Im weiteren Verlauf wurde das eigentliche Modell des Ansatzes
beschrieben, den event recording automata, welche eine determinierbare Subklasse
der timed automata darstellen. Im nächsten Abschnitt des Grundlagenkapitels wurde die symbolische Repräsentation eingeführt, welche den unendlichen Zustandsraum eines timed automata mithilfe der zones auf eine endliche Darstellung bringt
und gleichzeitig die Berechnung von zulässigen timed traces sowie den erreichbaren Zustandsraum ermöglicht. Im nächsten Kapitel wurde dann das Thema der
Testselektion beschrieben, welches wie schon angesprochen eine sehr wichtige Rolle
beim timed testing einnimmt. Im präsentierten Ansatz wurde die Selektion durch
den sogenannten Äquivalenzklassengraph durchgeführt, welcher den Zustandsraum
anhand der möglichen Uhrenwerte in Partitionen einteilt und jede Klasse mit den
angesprochenen deadlock-observations dekoriert. Im letzten Abschnitt wurde der
Gesamtalgorithmus beschrieben, welcher alle vorgestellten Techniken in Zusammenklang bringt und somit das algorithmische Vorgehen der gesamten Testerzeugung
beschreibt.
21
Literatur
[AlDi]
R. Alur und D. Dill. The theory of timed automata. In Real-Time:
Theory in Practice. Springer, S. 45–73.
[AlFH]
R. Alur, L. Fix und T. Henzinger. A determinizable class of timed automata. In Computer Aided Verification. Springer, S. 1–13.
[BBBr04] L. Brandan Briones und H. Brinksma. A test generation framework for
quiescent real-time systems-extended version. 2004.
[Dill89]
D. Dill. Timing assumptions and verification of finite-state concurrent
systems. In Automatic Verification Methods for Finite State Systems.
Springer, 1989, S. 197–212.
[KrTr04] M. Krichen und S. Tripakis. Black-box conformance testing for real-time
systems. Model Checking Software, 2004, S. 109–126.
[NiSk03] B. Nielsen und A. Skou. Automated test generation from timed automata. International Journal on Software Tools for Technology Transfer
(STTT), 5(1), 2003, S. 59–77.
[ScTr]
J. Schmaltz und J. Tretmans. On conformance testing for timed systems.
Formal Modeling and Analysis of Timed Systems, S. 250–264.
22

Download Report