Digitale Hardware/ Software-Systeme- P14

Chia sẻ: Cong Thanh | Ngày: | Loại File: PDF | Số trang:30

Thêm vào BST

Báo xấu

235
lượt xem 7
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Digitale Hardware/ Software-Systeme- P14:Getrieben durch neue Technologien und Anwendungen wird der Entwurf eingebetteter Systeme zunehmend komplexer. Dabei ist eine Umsetzung als Hardware/Software- System heutzutage der Stand der Technik. Die Minimierung von Fehlern im Entwurf dieser Systeme ist aufgrund deren Komplexit¨at eine der zentralen Herausforderungen unserer heutigen Zeit. Bereits heute wird mehr Aufwand in die Verifikation, also in die U¨ berpru¨fung der Korrektheit, eines eingebetteten Systems gesteckt als in den eigentlichen Entwurf....

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Digitale Hardware/ Software-Systeme- P14

384 7 Software-Veriﬁkation a) a b b) b a 1 1 s2 s3 1 f f tmp2 f 12 1 2 1 2 + + + s1 s4 t1 tmp1 tmp3 tmp4 1 2 1 2 + + s5 1 t2 c f tmp5 1 2 + t3 c Abb. 7.7. ADDG f¨ r a) Programm 1 und b) Programm 2 aus Beispiel 7.1.10 u Beispiel 7.1.13. F¨ r Programm 1 aus Beispiel 7.1.10 ergibt sich die Ausgabe-zu- u Eingabe-Abbildung f¨ r die Variablen c und b unter ausschließlicher Ber¨ cksichti- u u gung des rechten Pfades im ADDG in Abb. 7.7a) zu: ∗ Mc,b = Mc,tmp3 ◦ Mtmp3,tmp2 ◦ Mtmp2,b = {[d1 ] → [d2 ] | d1 = 3 · k ∧ d2 = k + 2 ∧ 128 ≤ k < 256 ∧ k ∈ Z} ¨ Aquivalenzpr¨ fung u ¨ Zur Aquivalenzpr¨ fung von zwei C-Programmen muss gezeigt werden, dass beide u Programme die selben Ausgaben f¨ r die selben Eingaben erzeugen. Unter der An- u nahme, dass beide Programme die selben Eingabe- und Ausgabevariablen besitzen, kann die Pr¨ fung in zwei Schritten durchgef¨ hrt werden. Dazu m¨ ssen die folgenden u u u u ¨ zwei Bedingungen auf ihre G¨ ltigkeit uberpr¨ ft werden: u 1. Die Menge der Ausgabe-zu-Eingabe-Abbildungen ist die selbe f¨ r beide Pro- u gramme.
¨ 7.1 Formale Aquivalenzpr¨ fung eingebetteter Software u 385 2. Die Berechnungen der beiden Programme sind identisch. Zusammen garantieren diese beiden Bedingungen, dass die Ausgaben beider Pro- gramme durch die selben Berechnungen auf den selben Eingabedaten entstehen. Da die ADDGs der beiden Programme Abstraktionen der Berechnungen der Programme ¨ darstellen, kann die Aquivalenzpr¨ fung auch mit Hilfe der ADDGs erfolgen. Dabei u werden die ADDGs der beiden Programme synchron von den Ausgabevariablen hin ¨ zu den Eingabevariablen traversiert. Die gesamte Aquivalenzpr¨ fung von zwei C- u Programmen ist nochmals in Abb. 7.8 zu sehen. Programm 1 Programm 2 ADDG- ADDG- Bestimmung Bestimmung ADDG 1 ADDG 2 Nein ¨ aquivalent? Diagnose Ja Programme ¨ aquivalent ¨ Abb. 7.8. Aquivalenzpr¨ fung zweier C-Programme mittels ADDGs [395] u Zun¨ chst wird die Traversierung der ADDGs f¨ r Programme gezeigt, die ledig- a u lich ein Propagieren von Ausdr¨ cken und Schleifentransformationen zur Optimie- u rung verwendet haben. Die synchrone Traversierung der ADDGs beginnt an korre- spondierenden Knoten der ADDGs, welche die selben Ausgabevariablen repr¨ sen- a tieren. Die Abh¨ ngigkeitsabbildung wird f¨ r beide Knoten mit der Identit¨ tsfunktion a u a initialisiert. Anschließend werden die beiden ADDGs synchron von den Ausgabeva- riablen zu den Eingabevariablen traversiert. Wenn dabei in einem ADDG eine interne Variable entdeckt wird, so wird diese eliminiert, d. h. die transitive Abh¨ ngigkeitsab- a bildung der Ausgaben wird mit der Abh¨ ngigkeitsabbildung der internen Variablen a konkateniert. Falls in einem ADDG ein Knoten erreicht wird, der eine Operation repr¨ sentiert, so muss ein Knoten mit der gleichen Operation als n¨ chstes auch im a a anderen ADDG erreicht werden. Dies kann allerdings auch erst nach einer Reihe weiterer interner Variablen erfolgen.
386 7 Software-Veriﬁkation Jedes Mal, wenn sich ein Pfad in einem ADDG verzweigt, m¨ ssen die passen- u den Pfade der beiden ADDGs bestimmt werden. Entspringt die Verzweigung ei- nem Operator-Knoten, so werden die Pfade mit der selben Beschriftung der bei- den ADDGs synchron weiterverfolgt. Entspringt die Verzweigung allerdings einem Variablenknoten, erfolgt die Zuordnung anhand der bisher berechneten transitiven Abh¨ ngigkeitsabbildung. a Zu jedem Zeitpunkt der Traversierung ist sichergestellt, dass auf den beiden kor- respondierenden Pfaden der ADDGs die selben Operationen berechnet wurden. Die u ¨ zweite Bedingung f¨ r die G¨ ltigkeit der Aquivalenzpr¨ fung ist bereits erf¨ llt, so- u u u bald ein Pfad bei einer Eingabevariable endet. Was noch zu zeigen ist, ist dass die Ausgabe-zu-Eingabe-Abbildungen der beiden Programme identisch sind. Dies ist automatisch gezeigt, wenn ersch¨ pfend f¨ r alle Pfade gezeigt wurde, dass die o u Ausgabe-zu-Eingabe-Abbildungen identisch sind. Damit ist bekannt, dass die selben Berechnungen auf den selben Eingabedaten zu den selben Ausgabedaten gef¨ hrt ha- u ¨ ben. Somit sind die beiden Programme aquivalent. Beispiel 7.1.14. Gegeben ist das folgende Schleifenprogramm [395]: 1 Programm 1 2 void prog1(int a[], int b[], int c[]) { 3 int k, tmp[1024], buf[2048]; 4 5 for (k=0; k=1; k--) 8 s2: buf[2*k-2] = a[2*k-2] + a[k-1]; 9 for (k=0; k
¨ 7.1 Formale Aquivalenzpr¨ fung eingebetteter Software u 387 Pfade im ADDG von Programm 2, welche aus der Aufteilung der Zuweisungen an die Variable c auf zwei Anweisungen t3 und t4 folgen. Nummeriert man die Pfade von links nach rechts, so gilt, dass Pfad 1 in Abb. 7.9a) mit den Pfaden 1 und 5 in Abb. 7.9b) korrespondiert. Die transitive Abh¨ ngigkeitsabbildung ergibt sich zu: a ∗ Mc,b = {[k] → [2k] | 0 ≤ k < 512 ∧ k ∈ Z} Weiterhin korrespondiert Pfad 2 in Abb. 7.9a) mit den Pfaden 2 und 6 in Abb. 7.9b), usw. a) b a b) b a 1 2 1 2 1 2 1 2 1 2 + + + + + s1 s2 t1 t2 tmp buf tmp buf 1 2 1 2 1 2 + + + s3 t3 t4 c c Abb. 7.9. ADDG von a) Programm 1 und b) Programm2 aus Beispiel 7.1.14 [395] ¨ Aquivalenzpr¨ fung mit algebraischen Transformationen u Im Folgenden werden C-Programme betrachtet, die zus¨ tzlich zum Propagieren von a Ausdr¨ cken und Schleifentransformationen durch algebraische Transformationen u entstanden sind. Algebraische Datenﬂusstransformationen nutzen Eigenschaften von Operationen und benutzerdeﬁnierten Funktionen aus, um das Programm zu optimie- ren, ohne die Funktionalit¨ t zu ver¨ ndern. Bei algebraischen Transformationen han- a a delt es sich um globale Transformationen, da diese nicht auf einzelne Anweisungen beschr¨ nkt sind. Viele dieser Transformationen basieren auf der Assoziativit¨ t bzw. a a Kommutativit¨ t von Operationen. a Die Auswirkung von algebraischen Transformationen sind in Abb. 7.10 zu se- hen. Wird eine kommutative Operation ⊗ berechnet, k¨ nnen die Operanden permu- o tiert werden (Abb. 7.10a)). Abbildung 7.10b) zeigt die m¨ gliche Gruppierung von o assoziativen Operationen ⊕. Ist eine Operation kommutativ und assoziativ, kann die Berechnung durch jeden m¨ glichen Baum aus der Operation gepaart mit jeder o m¨ glichen Permutation der Operanden berechnet werden (Abb. 7.10c)). o
388 7 Software-Veriﬁkation a) p1 p2 p2 p1 1 2 1 2 ⊗ ≡ ⊗ p p b) p1 p2 p2 p3 1 2 1 2 ⊕ p3 p1 ⊕ p1 p2 p3 1 2 1 2 1 2 3 ⊕ ≡ ⊕ ≡ ⊕ p p p c) p3 p4 1 2 p1 p2 p3 p4 p1 1 2 1 2 1 2 p2 p1 p2 p3 p4 1 2 1 2 1 2 3 4 ≡ ≡ p p p Abb. 7.10. Einﬂuss algebraischer Transformationen auf einen ADDG [395] Beispiel 7.1.15. Betrachtet wird wiederum Programm 1 aus Beispiel 7.1.14. Durch Anwendung algebraischer Transformationen erh¨ lt man Programm 3 [395]: a
¨ 7.1 Formale Aquivalenzpr¨ fung eingebetteter Software u 389 1 Programm 3 2 void prog3(int a[], int b[], int c[]) { 3 int k, buf[2048]; 4 5 for (k=0; k
390 7 Software-Veriﬁkation • Entfaltung: Wird bei der Traversierung ein assoziativer Operator ⊕ erkannt, wird eine Voraustraversierung durchgef¨ hrt, d. h. es wird eine geordnete Liste aus u Nachfolgerknoten aufgebaut, so dass die Knoten entweder Eingabevariablen oder Operationen repr¨ sentieren, die als erstes auf ⊕ folgen. Dadurch wird der ADDG a derart reduziert, dass die internen Variablen zwischen ⊕ und den direkt folgenden Operationen eliminiert wurden. • Zuordnung: Wird ein kommutativer Operator ⊗ in beiden ADDGs erreicht, kann die Beschriftung der ausgehenden Kanten nicht zur Zuordnung verwendet wer- den, da jede m¨ gliche Permutation der Operanden g¨ ltig ist. F¨ r die Zuordnung o u u wird in jedem ADDG f¨ r jeden Teil-ADDG, der Operator ⊗ als Quellknoten be- u sitzt, eine Traversierung durchgef¨ hrt, bis entweder die Eingabevariablen oder u Folgeoperationen erreicht wurden. Interne Variablen werden dabei eliminiert. Auf diese Art entsteht f¨ r jeden ADDG eine Liste von Nachfolgerknoten. Sind u diese eindeutig, k¨ nnen sie paarweise eins-zu-eins zugeordnet werden. Handelt o es sich bei mehrdeutigen Knoten um Eingabevariablen, erfolgt die Zuordnung ¨ uber Ausgabe-zu-Eingabe-Abbildungen. Handelt es sich um Operationsknoten, wird eine Voraustraversierung durchgef¨ hrt. u Beispiel 7.1.16. Bei dem Vergleich von Programm 1 und Programm 3 aus den Bei- spielen 7.1.14 und 7.1.15 wird zuerst die Addition in den beiden ADDGs erkannt. Aus diesem Grund muss eine Entfaltung vorgenommen werden. Die beiden resultie- renden ADDGs sind in Abb. 7.12 zu sehen. a) b a b) a b 1 2 3 4 1 2 3 4 + + c c Abb. 7.12. ADDG von a) Programm 1 aus Beispiel 7.1.14 und b) Programm 3 aus Bei- spiel 7.1.15 nach der Entfaltung [395] Die anschließende Zuordnung muss mit nicht eindeutigen Eingabevariablen um- gehen. Dies bedeutet, dass f¨ r jeden Pfad die Ausgabe-zu-Eingabe-Abbildung be- u rechnet werden muss. Diese ergeben sich wie folgt:
7.2 Testfallgenerierung zur simulativen Eigenschaftspr¨ fung u 391 Prog1 Prog3 ∗(1) ∗(4) Mc,b ⇔ Mc,b = {[k] → [2k] | k ∈ D} ∗(2) ∗(2) Mc,b ⇔ Mc,b = {[k] → [k] | k ∈ D} ∗(3) ∗(3) Mc,a ⇔ Mc,a = {[k] → [2k] | k ∈ D} ∗(4) ∗(1) Mc,a ⇔ Mc,a = {[k] → [k] | k ∈ D} Der Iterationsbereich ist gegeben als D = {[k] | 0 ≤ k ≤ 1024 ∧ k ∈ Z}. Weiterhin ist an den transitiven Abh¨ ngigkeitsabbildungen in Klammern immer der jeweilige a Pfad angegeben. ¨ 7.2 Testfallgenerierung zur simulativen Eigenschaftsprufung u ¨ F¨ r allgemeine Programme ist das Problem der Aquivalenzpr¨ fung nicht entscheid- u bar. Per Simulation kann jedoch ein Programm mit einem Referenzprogramm vergli- ¨ chen werden. Dabei ist das Ziel nicht, die Aquivalenz der Programme zu zeigen, son- dern deren unterschiedliches Verhalten aufzudecken. Dies kann, wie in Abschnitt 4.2 beschrieben, mit diversiﬁzierenden Methoden, z. B. auf Basis des Pfadbereichstest erfolgen. In diesem Abschnitt werden nun weitere Verfahren diskutiert, die zur Generie- a o a ¨ rung von Testf¨ llen verwendet werden k¨ nnen. Die Testf¨ lle lassen sich uber die ¨ Aquivalenzpr¨ fung hinaus zur funktionalen Eigenschaftspr¨ fung von Programmen u u einsetzen. Bei der Testfallgenerierung werden funktionsorientierte, kontrollﬂussori- entierte und datenﬂussorientierte Testf¨ lle unterschieden. Die beiden letzteren sind a Spezialformen der strukturorientierten Testf¨ lle. Die Verfahren zur Testfallgenerie- a ¨ rung werden im Folgenden zusammen mit den zugeh¨ rigen Uberdeckungsmaßen o eingef¨ hrt, die es erlauben, den Fortschritt der simulativen Veriﬁkation zu messen. u Die Darstellung erfolgt dabei in Anlehnung an [305]. 7.2.1 Funktionsorientierte Testf¨ lle a Grundlage f¨ r den funktionsorientierten Test bildet die Speziﬁkation. Diese wird u a ¨ herangezogen, um Testf¨ lle zu entwickeln, und um zu uberpr¨ fen, ob die Veriﬁkati- u on vollst¨ ndig ist, d. h. alle Funktionen auf deren korrekte Implementierung gepr¨ ft a u sind. Um dies quantitativ zu messen, k¨ nnen beispielsweise funktionale Eigenschaf- o ten des Systems als Zusicherungen formuliert werden. Bei der anschließenden Si- mulation mit den generierten Testfalleingaben wird dann gez¨ hlt, ob jede Zusicher- a ung mindestens einmal simuliert und dabei erf¨ llt wurde. In diesem Zusammenhang u spricht man auch davon, dass eine Zusicherung uberdeckt wurde. Der prozentuale ¨ ¨ Anteil aller uberdeckten Zusicherungen wird als Zusicherungs¨ berdeckung bezeich- u net. Oftmals liegen die funktionalen Anforderungen allerdings nicht als formale Zusi- cherungen vor. In diesem Fall k¨ nnen andere funktionsorientierte Testf¨ lle generiert o a werden.
392 7 Software-Veriﬁkation ¨ Funktionsorientierte Aquivalenzklassenbildung Die obige Darstellung zur Zusicherungs¨ berdeckung ist sehr vereinfacht dargestellt. u In realen Implementierungen werden komplexe Datentypen verwendet, die eine ¨ Uberpr¨ fung f¨ r jede m¨ gliche Variablenbelegung unm¨ glich machen. Aus diesem u u o o Grund muss eine Auswahl geeigneter Testf¨ lle vorgenommen werden, die repr¨ sen- a a tativ f¨ r alle m¨ glichen Variablenbelegungen ist. Neben dem Kriterium, dass die- u o se Testf¨ lle gute Repr¨ sentanten aller m¨ glichen Testf¨ lle darstellen, sollten diese a a o a dar¨ ber hinaus so gestaltet sein, dass zu erwartende Fehler zuverl¨ ssig aufgedeckt u a ¨ werden. Ein ahnliches Vorgehen wurde bereits bei der Testfallgenerierung f¨ r kom- u binatorische Schaltungen vorgestellt (siehe Abschnitt 6.1.2), bei denen ein zugrun- deliegendes Fehlermodell angenommen wurde. Ein Verfahren zur Testfallgenerierung nach dem Prinzip Teile und Herrsche“ ist ¨ ” die sog. funktionsorientierte Aquivalenzklassenbildung (siehe auch Abschnitt 4.2.1). ¨ Die funktionsorientierte Aquivalenzklassenbildung versucht, durch wiederholte Fall- unterscheidungen f¨ r Eingabe- und Ausgabebedingungen die Komplexit¨ t zu redu- u a ¨ zieren. Werte aus den resultierenden Aquivalenzklassen sollten dann zu einem aqui- ¨ valenten Verhalten der Implementierung f¨ hren. u ¨ Zur Bildung von Aquivalenzklassen unterscheidet man g¨ ltige und ung¨ ltige u u ¨ ¨ Aquivalenzklassen. G¨ ltige Aquivalenzklassen kennzeichnen Werte, die laut Spe- u u ¨ ziﬁkation zugelassen sind. Ung¨ ltige Aquivalenzklassen repr¨ sentieren dementspre- a chend Werte, die laut Speziﬁkation nicht auftreten d¨ rfen. Wird das System mit Wer- u ¨ ten aus ung¨ ltigen Aquivalenzklassen stimuliert, so liegt ein Fehlerfall vor und das u System muss mit einer entsprechenden Fehlerbehandlung reagieren. Erfolgt die Er- ¨ mittlung der Aquivalenzklassen anhand der Ausgabewerte, m¨ ssen anschließend die u Testf¨ lle so konstruiert werden, dass die Stimulation des Systems mit den zugeh¨ ri- a o ¨ gen Testfalleingaben zur Ausgabe in den entsprechenden Aquivalenzklassen f¨ hrt. u ¨ Die Auswahl der eigentlichen Testf¨ lle kann nach Bildung der Aquivalenzklas- a ¨ sen bez¨ glich unterschiedlicher Kriterien erfolgen. Ein ubliches Vorgehen basiert auf u der Grenzwertanalyse, bei der Werte direkt auf oder neben einer Grenze von Aqui- ¨ valenzklassen getestet werden. Die Idee hierbei ist, dass Fehler besonders h¨ uﬁg in a der N¨ he von Grenzen auftreten (siehe auch Abschnitt 4.2.1). Andere M¨ glichkeiten a o zur Auswahl der Testf¨ lle k¨ nnen beispielsweise auch zufallsbasiert sein. a o Ursache-Wirkungs-Analyse Die unabh¨ ngige Betrachtung von Eingabebereichen bzw. Ausgabebereichen ist in a ¨ komplexen Systemen h¨ uﬁg nicht ausreichend. Vielmehr stehen Aquivalenzklassen a typischerweise in Wechselwirkung miteinander. Dies bedeutet, dass Fehler h¨ uﬁg a nicht durch alleinige Betrachtung einer einzelnen Eingabe erzeugt werden k¨ nnen, o ¨ sondern bestimmte Wertekombinationen uber alle Eing¨ nge zu einem Fehlverhalten a ¨ f¨ hren. Allerdings ist es in der Praxis außerst schwierig diese Wechselwirkungen u festzustellen. Ein systematisches Verfahren zur Erzeugung von funktionsorientierten Testf¨ llen a unter Ber¨ cksichtigung von Wechselwirkungen ist unter dem Namen Ursache-Wirk- u ungs-Analyse (engl. cause-effect graphing) bekannt geworden. Dabei werden zu-
7.2 Testfallgenerierung zur simulativen Eigenschaftspr¨ fung u 393 ¨ n¨ chst die Beziehungen zwischen Aquivalenzklassen graphisch formuliert und an- a schließend in einem tabellarischen Verfahren geeignete Testf¨ lle ausgew¨ hlt. Die a a Ursache-Wirkungs-Analyse verl¨ uft in vier Schritten [305]: a 1. In einem anf¨ nglichen Schritt wird die Speziﬁkation in handhabbare Teile zer- a legt, da die Betrachtung von Wertekombinationen den Suchraum explodieren l¨ sst. a 2. F¨ r jede Teilspeziﬁkation werden Ursachen und Wirkungen identiﬁziert. Dabei u stellen Ursachen und Wirkungen Pr¨ dikate dar und besitzen somit den Wert T a oder F. Ursachen sind dabei einzelne Eingabebedingungen oder eine Aquiva- ¨ lenzklasse, z. B. die Variable x ≥ 10. Eine Wirkung ist eine Ausgabebedingung. 3. Erstellung eines Ursache-Wirkungs-Graphen, der die logischen Beziehungen von Ursachen und Wirkungen darstellt. Es handelt sich hierbei im Wesentli- chen um ein Boolesches Netzwerk, das durch Transformation der Speziﬁkati- on gewonnen wird. Es werden dabei aber auch Abh¨ ngigkeiten zwischen den a Ursachen und/oder Wirkungen, die sich aus Umgebungsbedingungen ergeben, ber¨ cksichtigt. u 4. Der Ursache-Wirkungs-Graph wird in eine sog. Entscheidungstabelle umge- formt und f¨ r jede Spalte der Tabelle eine Testfalleingabe erzeugt. u Der Ursache-Wirkungs-Graph kann als Boolesches Netzwerk betrachtet und re- pr¨ sentiert werden. Es wird hier dennoch die in [305] verwendete, kompakte Re- a pr¨ sentation verwendet. In Ursache-Wirkungs-Graphen stehen Ursachen links und a Wirkungen rechts. Die wesentlichen Beziehungen zwischen Ursachen und/oder Wir- kungen sind in Abb. 7.13 dargestellt. a) d) f) h) ∧ O M b) c) e) g) i) ∨ E I R Abb. 7.13. Beziehungen zwischen Ursachen und/oder Wirkungen [305]
394 7 Software-Veriﬁkation Falls eine Ursache und eine Wirkung stets den selben Wert besitzen, so besteht zwischen Ursache und Wirkung eine Identit¨ t (siehe Abb. 7.13a)). Falls Ursache und a Wirkung jedoch stets invertierte Werte zueinander besitzen, so ist deren Relation ei- ne Negation (Abb. 7.13b)). Eine Disjunktion (Konjunktion) liegt vor, wenn eine Wir- kung eintritt, sofern eine (alle) der verbundenen Ursachen eintreten (Abb. 7.13c) und d)). Eine exklusive Beziehung zwischen zwei Ursachen besteht, wenn die Anwesen- heit einer Ursache die Anwesenheit der anderen Ursache ausschließt (Abb. 7.13e)). Die O-Abh¨ ngigkeit (engl. one, and only one) ist gegeben, wenn immer exakt eine a Ursache erf¨ llt ist (Abb. 7.13f)). Abbildung 7.13g) zeigt eine inklusive Beziehung u zwischen Ursachen. Dies bedeutet, dass mindestens immer eine Ursache erf¨ llt ist. u Die R- und M-Abh¨ ngigkeit (engl. requires und masks), dargestellt in Abb. 7.13h) a und i), liegen vor, falls die Anwesenheit einer Ursache die Anwesenheit der anderen Ursache voraussetzt, bzw. die Anwesenheit der Ursache durch die Anwesenheit der anderen Ursache maskiert wird. Das folgende Beispiel stammt aus [305]. Beispiel 7.2.1. Betrachtet wird ein Programm, das Zeichen von einer Tastatur solan- ge einliest, wie große Vokale und große Konsonanten eingegeben werden oder ein Z¨ hler kleiner ist als der Maximalwert vom Typ int. Der Z¨ hler wird beim Lesen a a eines großen Vokals oder Konsonanten inkrementiert. Er z¨ hlt somit die gelesenen a Zeichen. Im Falle, dass das gelesene Zeichen ein großer Vokal ist, wird ein zweiter Z¨ hler f¨ r die Vokale ebenfalls inkrementiert. Ist das gelesene Zeichen weder ein a u großer Vokal noch ein großer Konsonant, so wird das Programm beendet. Das Pro- gramm sieht wie folgt aus: 1 Programm 2 char c; 3 int count = 0; 4 int voc_count = 0; 5 std::cin >> c; 6 while((c >= ’A’) && (c > c; 13 } Die Ursachen in diesem Programm lauten: • u1 : das gelesene Zeichen ist ein großer Konsonant • u2 : das gelesene Zeichen ist ein großer Vokal • u3 : der Z¨ hler f¨ r die gelesenen Zeichen ist kleiner dem maximalen Wert vom a u Typ int Die Wirkungen in diesem Programm lauten: • w1 : der Z¨ hler f¨ r die gelesenen Zeichen wird inkrementiert a u • w2 : der Z¨ hler f¨ r die gelesenen Vokale wird inkrementiert a u
7.2 Testfallgenerierung zur simulativen Eigenschaftspr¨ fung u 395 • w3 : das Zeichen wird gelesen • w4 : das Programm wird beendet Der Ursache-Wirkungs-Graph f¨ r dieses Programm ist in Abb. 7.14 zu sehen. u u1 E ∨ z1 ∧ w1 u2 ∧ w2 ∧ w3 ∧ w4 u3 Abb. 7.14. Ursache-Wirkungs-Graph f¨ r das Programm aus Beispiel 7.2.1 [305] u Man erkennt, dass sich die Ursachen u1 und u2 gegenseitig ausschließen. Durch die Disjunktion beider Ursachen wird eine Zwischenursache z1 generiert, die den Wert T annimmt, sobald ein großer Konsonant oder großer Vokal eingegeben wurde. Weiterhin sieht man, dass die Wirkungen w1 und w3 von exakt den selben Ursachen abh¨ ngen. Die Wirkung w4 tritt immer genau dann ein, wenn w1 bzw. w3 nicht auf- a treten und umgekehrt. Aus diesem Grund ist es ausreichend, Testfalleingaben f¨ r die u a ¨ Wirkungen w1 und w2 zu erzeugen. Diese Testf¨ lle uberpr¨ fen automatisch auch die u Wirkungen w3 und w4 . Nach Erstellung des Ursache-Wirkungs-Graphen erfolgt die Umwandlung in ei- ne Entscheidungstabelle. Dies geschieht durch die folgenden vier Schritte [305]: 1. Auswahl einer Wirkung im Ursache-Wirkungs-Graphen. 2. Identiﬁkation von Kombinationen von Ursachen, welche die Wirkung erzeugen bzw. nicht erzeugen. 3. F¨ r jede gefundene Kombination von Ursachen wird eine Spalte in der Entschei- u ¨ dungstabelle erstellt, die ebenfalls alle Werte der ubrigen Wirkungen enth¨ lt. a 4. Entfernung mehrfach vorkommender Eintr¨ ge aus der Entscheidungstabelle a Die Identiﬁkation der Kombinationen von Ursachen erfolgt durch Bestimmung m¨ glicher Eingabewerte anhand der Ausgabewerte von (Zwischen-)Ursachen. Be- o sitzt beispielsweise der Ausgang einer Konjunktion den Wert T, so m¨ ssen alle u Eing¨ nge auf den Wert T gesetzt werden. Analog m¨ ssen bei einer Disjunktion a u mit Ausgabe F alle Eing¨ nge auf F gesetzt werden. Komplizierter ist es, wenn der a
396 7 Software-Veriﬁkation Ausgang der Disjunktion den Wert T tr¨ gt. In diesem Fall m¨ ssen alle Eingaben a u ber¨ cksichtigt werden, wobei genau ein Eingang den Wert T tr¨ gt und alle anderen u a Eing¨ nge den Wert F. Durch diese Regel werden Fehlermaskierungen vermieden. a Schließlich m¨ ssen bei einer Konjunktion mit Ausgabe F alle Eingaben ber¨ cksich- u u tigt werden, bei denen genau ein Eingang auf F gesetzt ist und alle anderen Eing¨ nge a auf T. Durch diese Regel sollen wiederum Fehlermaskierungen vermieden werden. Beispiel 7.2.2. Betrachtet wird das Programm aus Beispiel 7.2.1. Der Ursache-Wir- kungs-Graph ist in Abb. 7.14 zu sehen. Man kann sehen, dass die Wirkungen w1 , w3 und w4 gemeinsam betrachtet werden k¨ nnen. Repr¨ sentativ hierf¨ r wird die Wir- o a u kung w1 betrachtet. Die Wirkung w1 tritt ein, wenn die Ursache u3 und die Zwi- schenursache z1 auftreten. Damit die Zwischenursache z1 auftritt, muss Ursache u1 oder Ursache u2 erf¨ llt sein. Aufgrund der oben genannten Regel (aber auch auf- u grund der Exklusivit¨ t der beiden Ursachen) sind die zu betrachtenden Belegungen a (u1 = T) ∧ (u2 = F) sowie (u1 = F) ∧ (u2 = T). Das Nichteintreten von Wirkung w1 resultiert zun¨ chst in den Belegungen (z1 = a T) ∧ (u3 = F) sowie (z1 = F) ∧ (u3 = T). Aus z1 = F folgt direkt, dass die beiden Ursachen u1 und u2 in diesem Testfall nicht erf¨ llt sein d¨ rfen. F¨ r den Fall z1 = T u u u ergeben sich wiederum die beiden Kombinationen (u1 = T) ∧ (u2 = F) sowie (u1 = F) ∧ (u2 = T). Nach den selben Regeln k¨ nnen nun noch die Testfalleingaben f¨ r o u w2 = F und w2 = T erzeugt werden. Die resultierende Entscheidungstabelle ist in Tabelle 7.1 dargestellt. Tabelle 7.1. Entscheidungstabelle f¨ r das Programm aus Beispiel 7.2.1 [305] u Testf¨ lle a Kommentar 1 2 3 4 5 u1 T F F F F großer Konsonant Ursache u2 F TFTF großer Vokal u3 T TTF F < MAX INT z1 T TFTT w1 T TF F F Z¨ hler wird inkrementiert a w2 F TF F F Vokalz¨ hler wird inkrementiert a Wirkung w3 T TF F F Zeichen wird gelesen w4 F FTTT Programm wird beendet Zustandsorientierte Testf¨ lle a ¨ Die beschriebene Aquivalenzklassenbildung arbeitet alleinig auf den Wertebereichen ¨ der Ein- oder Ausgaben eines Systems. Wenn unter Verwendung von Aquivalenz- klassen f¨ r Ausgabewertebereiche Testfalleingaben generiert werden sollen, stellt u sich allerdings die Frage, ob das System zustandsbehaftet ist, oder nicht. Spezielle
7.2 Testfallgenerierung zur simulativen Eigenschaftspr¨ fung u 397 Verfahren zur Erstellung funktionsorientierter Testf¨ lle, die auf Verhaltensspeziﬁ- a kationen als endliche Automaten basieren, werden als Verfahren zur Erstellung zu- standsorientierter Testf¨ lle bezeichnet. Da der endliche Automat das Verhalten (die a Funktion) des Systems speziﬁziert, handelt es sich hierbei um funktionsorientierte Testf¨ lle. a Die einfachste M¨ glichkeit zustandsorientierte Testf¨ lle zu erstellen, besteht dar- o a in, Eingaben so zu w¨ hlen, dass jeder Zustand mindestens einmal besucht wird. Es a wird somit eine 100%-ige Zustands¨ berdeckung gefordert. Ein Auswahlkriterium f¨ r u u zustandsbasierte Testf¨ lle, das zu einer h¨ heren Veriﬁkationsvollst¨ ndigkeit f¨ hrt, ist a o a u die Forderung, jeden Zustands¨ bergang mindestens einmal zu gehen. Das Ziel ist so- u ¨ mit eine 100%-ige Ubergangs¨ berdeckung zu erreichen. Man beachte, dass 100 Pro- u ¨ zent Ubergangs¨ berdeckung 100% Zustands¨ berdeckung implizieren. Ubergangs- u u ¨ bedingungen an Zustands¨ berg¨ ngen k¨ nnen aus disjunktiv verkn¨ pften Ereignissen u a o u ¨ bestehen. Da eine 100%-ige Ubergangs¨ berdeckung nicht garantiert, dass jedes Er- u eignis einmal getestet wurde, kann ein weiteres Auswahlkriterium f¨ r Testf¨ lle sein, u a eine m¨ glichst hohe Ereignis¨ berdeckung zu erreichen. Man beachte, dass wieder- o u u ¨ um eine 100%-ige Ereignis¨ berdeckung eine 100%-ige Ubergangs¨ berdeckung und u ¨ somit eine 100%-ige Zustands¨ berdeckung impliziert. Diese drei Uberdeckungsar- u ten f¨ r zustandsorientierte Testf¨ lle bilden somit eine Hierarchie, die in Abb. 7.15 u a ¨ zu sehen ist. Die Uberdeckungsmaße f¨ r zustandsorientierte Testf¨ lle wird anhand u a eines Beispiels aus [305] verdeutlicht. alle Ereignisse alle Zustands¨ berg¨ nge u a alle Zust¨ nde a ¨ Abb. 7.15. Uberdeckungshierarchie f¨ r zustandsorientierte Testf¨ lle [305] u a Beispiel 7.2.3. Es wird der Verbindungsaufbau und -abbau beim Telefonieren be- trachtet. Der endliche Zustandsautomat ist in Abb. 7.16 dargestellt. Die einzelnen Zust¨ nde haben darin die folgende Bedeutung: a Zustand Bedeutung s0 Verbindung ist getrennt s1 W¨ hlend a s2 Verbindung hergestellt s3 Ung¨ ltige Nummer gew¨ hlt u a s4 Timeout aufgetreten Der Anfangszustand ist der Zustand s0 . Sobald der W¨ hlvorgang durch Abheben a (Ereignis eab ) begonnen wurde, dieser aber noch nicht beendet wurde, beﬁndet sich
398 7 Software-Veriﬁkation das Telefon im Zustand s1 . In diesem Zustand kann der Benutzer Ziffern w¨ hlen a (Ereignisse e0 bis e9 ) und diese werden an die Rufnummer angeh¨ ngt (ez ) und auf a Plausibilit¨ t gepr¨ ft (e p ). Wurde eine g¨ ltige Rufnummer gew¨ hlt (erg ), so wird die a u u a Verbindung aufgebaut (evau f ). Dies wird durch den Wechsel in Zustand s2 dargestellt. a u ¨ Ist die gew¨ hlte Rufnummer hingegen ung¨ ltig (eru ), so erfolgt der Ubergang in Zustand s3 . Das Auﬂegen (eau f ) f¨ hrt in jedem Zustand zum vollst¨ ndigen Abbruch u a des Telefonats und dem Zur¨ cksetzen des Automaten (Zustand s0 und Ereignis er ). u Im Zustand s2 f¨ hrt es zus¨ tzlich dazu, dass die Verbindung abgebaut wird (evab ). u a Schließlich kann es noch in den Zustanden s1 und s3 zu der Situation kommen, dass der Benutzer keinerlei Eingaben mehr t¨ tigt. Ein Timeout eto wird verwendet, um a das Telefonat zu beenden. Hierzu wird der Zwischenzustand s4 betreten. eto /er s4 eau f eto /er eab /er s1 s0 e 0 . . . e9 eau f /er /ez ∧ e p erg/evau f s2 eau f /er ∧evab eru s3 eau f /er Abb. 7.16. Endlicher Zustandsautomat f¨ r den Verbindungsaufbau und - abbau u An diesem Beispiel kann man erkennen, dass eine 100%-ige Zustands¨ berde- u ¨ ckung keine 100%-ige Ubergangs¨ berdeckung garantiert. Durch die beiden Testfal- u leingaben eab , erg und eab , eru , eto werden zwar alle Zust¨ nde besucht, aber le- a diglich eine Ubergangs¨ berdeckung von 10 = 40% erreicht. Eine Ubergangs¨ berde- ¨ u 4 ¨ u ckung von 100% k¨ nnte beispielsweise durch die folgenden sechs Testfalleingaben o erzielt werden: eab , eau f eab , eto , eau f eab , eto , eau f eab , e0 , erg , eau f eab , e8 , eru , eau f eab , e8 , eru , eto , eau f Hierdurch ist allerdings noch keine 100%-ige Ereignis¨ berdeckung erzielt worden. u Um dies zu erreichen, m¨ sste im Zustand s1 jede Ziffer mindestens einmal gew¨ hlt u a werden und somit den Zustands¨ bergang zur¨ ck zu s1 ausl¨ sen. u u o
7.2 Testfallgenerierung zur simulativen Eigenschaftspr¨ fung u 399 Der in Abb. 7.16 dargestellte endliche Automat ist nicht vollst¨ ndig speziﬁziert, a d. h. nicht alle Reaktionen auf jedes Ereignis in jedem Zustand wurden speziﬁziert. Der Automat beschreibt somit lediglich das erwartete Verhalten des Telefons. Dies bedeutet aber auch, dass die zustandsorientierten Testf¨ lle lediglich die Normalf¨ lle a a ¨ uberpr¨ fen. Fehlersituationen werden ignoriert. u Zur Erzeugung zustandsorientierter Testf¨ lle f¨ r den Fehlerfall bietet es sich an, a u den endlichen Automaten als Automatentabelle zu repr¨ sentieren. In einer Automa- a tentabelle wird mit jeder Zeile ein Zustand und mit jeder Spalte ein Ereignis assozi- iert. Bei den Ereignissen kann es sich dabei auch um zusammengesetzte Ereignisse handeln. In den Feldern der Tabelle, die Kreuzungspunkte zwischen Zust¨ nden und a Ereignissen darstellen, werden der Folgezustand und die Ausgabe eingetragen, wenn in dem gegeben Zustand das angegebene Ereignis auftritt. Ist der zugrundeliegende endliche Automat nicht vollst¨ ndig speziﬁziert, ist diese Tabelle ebenfalls unvoll- a st¨ ndig, da Felder leer bleiben. a Um eine vollst¨ ndige Ereignis¨ berdeckung auch f¨ r Fehlerf¨ lle zu erreichen, ist a u u a es notwendig, jedes Tabellenfeld in einem Testfall zu ber¨ cksichtigen. Man kann da- u bei annehmen, dass das Auftreten nicht speziﬁzierter Ereignisse in einem Zustand zu einem Verhalten f¨ hrt, in dem der endliche Automat in dem selben Zustand verbleibt u und keine Ausgabe erzeugt. Unter dieser Annahme k¨ nnen die leeren Tabellenfelder o gef¨ llt und somit ein vollst¨ ndig speziﬁzierter endlicher Automat geschaffen wer- u a den. Werden nun Testfalleingaben so erzeugt, dass jedes Tabellenfeld ber¨ cksichtigt u wird, so kann man eine 100%-ige Ereignis¨ berdeckung f¨ r die Normal- und Feh- u u lerf¨ lle erzielen. a Beispiel 7.2.4. Betrachtet wird der Zustandsautomat aus Abb. 7.16 aus Beispiel 7.2.3. Die vollst¨ ndige Automatentabelle ist in Tabelle 7.2 gezeigt. Die Eintr¨ ge in den Ta- a a bellenfelder sind von der Form Folgezustand/Ausgabe. Tabelle 7.2. Vollst¨ ndige Automatentabelle zum endlichen Automaten aus Abb. 7.16 [305] a eab eau f e0 ... e9 eto erg eru s0 s1 /er s0 / s0 / s0 / s0 / s0 / s0 / s1 s1 / s0 /er s1 /ez ∧ e p s1 /ez ∧ e p s4 /er s2 /evau f s3 / s2 s2 / s0 /er ∧ evab s2 / s2 / s2 / s2 / s2 / s3 s3 / s0 /er s3 / s3 / s4 /er s3 / s3 / s4 s4 / s0 / s4 / s4 / s4 / s4 / s4 / Im Allgemeinen wird man bei der Generierung zustandsbasierter Testf¨ lle drei a Arten von Ereignissen unterscheiden [305]: 1. Ereignisse, die, falls sie in einem Zustand auftreten, einen Zustandswechsel und/oder eine Ausgabe bewirken, 2. Ereignisse, die, falls sie in einem Zustand auftreten, ignoriert werden und
400 7 Software-Veriﬁkation 3. Ereignisse, die, falls sie in einem Zustand auftreten, einer Fehlerbehandlung er- forderlich machen. Letztere kann man beispielsweise durch einen speziellen Fehlerzustand se behan- deln. Beispiel 7.2.5. F¨ r das Telefon aus Beispiel 7.2.3 k¨ nnen im Anfangszustand s0 u o die Ereignisse e0 , . . . , e9 , die das Dr¨ cken einer Ziffer signalisieren, und das Auf- u legen (eau f ) ignoriert werden. Ein Auftreten eines Timeouts (eto ) oder das Auftreten der Ereignisse erg und eru , die eine g¨ ltige bzw. ung¨ ltige Rufnummer repr¨ sen- u u a tieren, ist als Fehlerfall zu werten. Die vollst¨ ndige Automatentabelle (ohne Zu- a stands¨ berg¨ nge in Zustand s2 ) ist in Tabelle 7.3 zu sehen. u a Tabelle 7.3. Vollst¨ ndige Automatentabelle zum endlichen Automaten aus Abb. 7.16 mit Feh- a lerzustand se [305] eab eau f e0 ... e9 eto erg eru s0 s1 /er s0 / s0 / s0 / se / se / se / s1 s1 / s0 /er s1 /ez ∧ e p s1 /ez ∧ e p s4 /er s2 /evau f s3 / s2 s2 / s0 /er ∧ evab s2 / s2 / se / se / se / s3 s3 / s0 /er s3 / s3 / s4 /er se / se / s4 s4 / s0 / s4 / s4 / s4 / se / se / 7.2.2 Kontrollﬂussorientierte Testf¨ lle a Neben funktionsorientierten Testf¨ llen, die sich an der Speziﬁkation eines Systems a orientieren, gibt es eine zweite große Klasse an Testf¨ llen, die sog. strukturorientier- a ten Testf¨ lle. Wie der Name bereits suggeriert, werden diese anhand von Strukturmo- a dellen, also Implementierungen, erstellt. Die Klasse der strukturorientierten Testf¨ lle a l¨ sst sich wiederum in zwei Unterklassen einteilen, die sog. kontrollﬂussorientierten a und die sog. datenﬂussorientierten Testf¨ lle. Die Verwendung von strukturorientier- a ten Testf¨ llen in der simulativen Veriﬁkation hat allerdings zum Nachteil, dass spezi- a ﬁzierte, aber nicht implementierte Funktionen nicht entdeckt werden k¨ nnen. Hierzu o ist es notwendig auf funktionsorientierte Testf¨ lle zur¨ ckzugreifen. a u Zun¨ chst werden die kontrollﬂussorientierten Testf¨ lle n¨ her betrachtet. Diese a a a arbeiten auf Kontrollﬂussgraphen, die aus Programmen extrahiert werden. F¨ r die u Erstellung der Testf¨ lle werden unterschiedliche Aspekte der Programmabarbeitung a verwendet, z. B. Anweisungen, Zweige, Bedingungen, Schleifen oder Pfade. Ziel bei der Erstellung kontrollﬂussorientierter Testf¨ lle ist es immer, eine m¨ glichst hohe a o ¨ ¨ Uberdeckung dieser Aspekte zu erzielen. Aus diesem Grund werden Uberdeckungs- maße f¨ r diese Aspekte als Vollst¨ ndigkeitskriterium der mit diesen Testfalleingaben u a durchgef¨ hrten simulativen Veriﬁkation verwendet. Simulative Veriﬁkationsverfah- u ¨ ren, die ein Uberdeckungsmaß als Vollst¨ ndigkeitskriterium beinhalten, werden aus a
7.2 Testfallgenerierung zur simulativen Eigenschaftspr¨ fung u 401 ¨ historischen Gr¨ nden als Uberdeckungstests bezeichnet. Die Erstellung datenﬂuss- u orientierter Testf¨ lle wird anschließend in Abschnitt 7.2.3 beschrieben. a ¨ Anweisungsuberdeckungstest Die einfachsten kontrollﬂussorientierten Testf¨ lle werden so entwickelt, dass eine a m¨ glichst hohe Anweisungs¨ berdeckung (engl. statement coverage) erzielt wird. So- o u mit ist das Ziel, jede Anweisung in einem Programm mindestens einmal auszuf¨ hren. u Diese Vorgehensweise ist einleuchtend, da sie sicherstellt, dass das Programm keinen unerreichbaren Quelltext (engl. dead code) enth¨ lt. Die Anweisungs¨ berdeckung CS a u ist wie folgt deﬁniert: |{ausgef¨ hrte Anweisungen}| u CS = (7.1) |{Anweisungen}| Es wird also der Anteil ausgef¨ hrter Anweisungen aller Anweisungen bestimmt. Das u Ziel ist es, 100% Anweisungs¨ berdeckung zu erzielen. Die zugeh¨ rige simulative u o Veriﬁkation wird als Anweisungs¨ berdeckungstest bezeichnet. u Beispiel 7.2.6. Gegeben ist das folgende Fragment eines C-Programms: 1 a = b + c; 2 x = y; 3 if (a > x) { 4 y = b; 5 x = x + 2; 6 } else 7 b = b + c; 8 if (x == y) 9 c = y; 10 else 11 y = a; Dieses Programm enth¨ lt neun Anweisungen (die Zeilen 6 und 10 enthalten kei- a ne Anweisungen). Betrachtet wird die Testfalleingabe (b = 1) ∧ (c = 1) ∧ (y = 1). Durch Simulation kann man bestimmen, dass die Anweisungen 1, 2, 3, 4, 5, 8, 11 , also sieben der neun vorhandenen Anweisungen, ausgef¨ hrt werden. Die durch die- u se Testfalleingabe erzielte Anweisungs¨ berdeckung betr¨ gt somit CS = 7 . Um 100% u a 9 Anweisungs¨ berdeckung zu erreichen, wird eine zweite zus¨ tzliche Testfalleingabe u a ben¨ tigt. Dies k¨ nnte beispielsweise (b = 0)∧(c = 0)∧ (y = 1) sein. In der Simulati- o o on dieses Testfalls werden die Anweisungen 1, 2, 3, 7, 8, 9 ausgef¨ hrt. Die alleinige u Anweisungs¨ berdeckung dieses Testfalls betr¨ gt somit CS = 6 . Beide Testfalleinga- u a 9 ben zusammen f¨ hren allerdings 100% der Anweisungen aus, weshalb CS = 1 ist. u Sicherlich ist eine 100%-ige Anweisungs¨ berdeckung ein notwendiges Kriteri- u um, um Fehler, die in Anweisungen enthalten sind, zu pr¨ fen. Allerdings handelt es u sich nicht um ein hinreichendes Kriterium, um Fehler in Anweisungen zu erkennen, da ein Fehler eventuell nur unter bestimmten Stimuli auftritt.
402 7 Software-Veriﬁkation Beispiel 7.2.7. Angenommen das Programm in Beispiel 7.2.6 enthalte in Zeile 3 einen Fehler: Anstelle von (a > x) muss es korrekterweise (a >= x) heißen. Kei- ner der beiden Testfalleingaben aus Beispiel 7.2.6 ((b = 1) ∧ (c = 1) ∧ (y = 1) und (b = 0)∧(b = 0)∧(y = 1)) ist in der Lage diesen Fehler aufzudecken, obwohl sie zu- sammen eine 100%-ige Anweisungs¨ berdeckung hervorrufen. Eine geeignete Test- u falleingabe, um diesen Fehler zu entdecken, w¨ re beispielsweise ((b = 1) ∧ (c = a 0) ∧ (y = 1), da dies zu einer identischen Wertzuweisung von a und x in Zeile 3 des Programms f¨ hrt. u Man muss allerdings auch bei diesem Beispiel ber¨ cksichtigen, dass der Fehler u nicht nur steuerbar, sondern auch beobachtbar sein muss, so dass dieser entdeckt wer- den kann. Der Fehler muss sich also in der Ausgabe des Programms niederschlagen. ¨ Zweiguberdeckungstest Der Anweisungs¨ berdeckungstest hat zum Ziel, 100% Anweisungs¨ berdeckung zu u u erreichen. Dies ist gleichbedeutend mit der Aussage, dass in dem Kontrollﬂussgra- phen alle Knoten mindestens einmal durchlaufen werden. Ein wesentlich wichtigeres Maß ist allerdings die Zweig¨ berdeckung (engl. branch coverage), die misst, wie vie- u le Kanten des Kontrollﬂussgraphen durchlaufen werden. Der zugeh¨ rige Zweig¨ ber- o u deckungstest, der eine 100%-ige Zweig¨ berdeckung zum Ziel hat, subsumiert den u Anweisungs¨ berdeckungstest, d. h. eine Zweig¨ berdeckung von 100% impliziert u u eine 100%-ige Anweisungs¨ berdeckung. Die Zweig¨ berdeckung CB l¨ sst sich als u u a Quotient aus durchlaufenen Kanten zur Gesamtanzahl aller Kanten im Kontrollﬂuss- graphen ausdr¨ cken: u |{ausgef¨ hrte Kontrollﬂusskanten}| u CB = (7.2) |{Kontrollﬂusskanten}| Der Zweig¨ berdeckungstest hat zwei Ziele: Zum einen sollen Kontrollﬂusskan- u ten identiﬁziert werden, die nicht durchlaufen werden k¨ nnen. Zum anderen sollen o Kontrollﬂusskanten identiﬁziert werden, die sehr h¨ uﬁg durchlaufen werden. Letzte- a re k¨ nnen f¨ r die Programmoptimierung verwendet werden. Werden Kontrollﬂuss- o u kanten nicht durchlaufen, kann dies prinzipiell zwei Gr¨ nde haben: Entweder kann u der Zweig des Programms nicht durchlaufen werden, d. h. es existieren keine Testfal- leingaben, die bewirken, dass der Programmzweig durchlaufen wird, oder es konn- te bisher keine geeignete Testfalleingabe konstruiert werden, obwohl eine existiert. Letzteres tritt besonders h¨ uﬁg ein, wenn Umgebungswerte in dem eingebetteten a System verarbeitet werden, die sich nicht direkt steuern lassen. Existieren allerdings keine Testfalleingaben, um einen Programmzweig zu durchlaufen, so liegt ein Ent- wurfsfehler vor. Beispiel 7.2.8. Betrachtet wird das Programm aus Beispiel 7.2.1 auf Seite 394 zum Z¨ hlen der großen Konsonanten und Vokale in einer Eingabe. Der Kontrollﬂussgraph a
7.2 Testfallgenerierung zur simulativen Eigenschaftspr¨ fung u 403 ist in Abb. 7.17 dargestellt. Eine Testfalleingabe, die 100% Zweig¨ berdeckung er- u zeugt, w¨ re beispielsweise die Eingabesequenz ’A’, ’B’, ’1’ . Die durchlaufene a Sequenz an Zust¨ nden in dem Kontrollﬂussgraphen lautet bei Simulation mit dieser a Testfalleingabe v1 , v2 , v3 , v4 , v5 , v2 , v3 , v5 , v2 , v6 . v1 v2 else (c >= ’A’) && (c