Digitale Hardware/ Software-Systeme- P15

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

Thêm vào BST

Báo xấu

64
lượt xem 3
download

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

Digitale Hardware/ Software-Systeme- P15: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- P15

414 7 Software-Veriﬁkation ¨ all p-uses-Uberdeckungstest ¨ Im all p-uses-Uberdeckungstest wird gefordert, dass f¨ r jede Entscheidung und f¨ r u u jede darin verwendete Variable jede Kombination mit deren Deﬁnitionen, welche die Entscheidung erreichen, gepr¨ ft wird. Die Testf¨ lle m¨ ssen also das folgende Krite- u a u rium erf¨ llen: F¨ r jeden Knoten vi im datenﬂussattributierten Kontrollﬂussgraph und u u jeder Variablen x ∈ de f s(vi ) muss mindestens ein deﬁnitionsfreier Pfad bez¨ glich x u von Knoten vi zu jeder Kante in dpu(x, vi ) getestet werden. Beispiel 7.2.20. Betrachtet wird das Programm aus Beispiel 7.2.16. Um 100% all p-uses-Uberdeckung zu erzielen, sind zwei Testfalleingaben notwendig: (vin , v1 , v3 , ¨ vout ) und (vin , v1 , v2 , v3 , vout ). Damit werden die beiden Kanten (v1 , v3 ) und (v1 , v2 ), die mit p-uses attributiert sind, getestet. ¨ Somit subsumiert der all p-uses-Uberdeckungstest den Zweig¨ berdeckungstest. u ¨ all c-uses-Uberdeckungstest ¨ ¨ Analog zum all p-uses-Uberdeckungstest wird im all c-uses-Uberdeckungstest ge- fordert, dass f¨ r jeden globalen berechnenden Zugriff und f¨ r jede darin verwendete u u Variable jede Kombination mit deren Deﬁnitionen, die den Zugriff erreichen, gepr¨ ft u wird. Die Testf¨ lle m¨ ssen somit das folgende Kriterium erf¨ llen: F¨ r jeden Knoten a u u u vi im datenﬂussattributierten Kontrollﬂussgraph und jeder Variablen x ∈ de f s(vi ) muss mindestens ein deﬁnitionsfreier Pfad bez¨ glich x von Knoten vi zu jedem Kno- u ten in dcu(x, vi ) getestet werden. Beispiel 7.2.21. F¨ r das Programm aus Beispiel 7.2.16 f¨ hrt die Testfalleingabe u u (vin , v1 , v2 , v3 , vout ) zu einer 100%-igen all c-uses-Uberdeckung. ¨ ¨ Der all c-uses-Uberdeckungstest subsumiert weder Zweig-, Anweisungs- noch ¨ einen anderen defs/uses-Uberdeckungstest. ¨ all c-uses/some p-uses-Uberdeckungstest ¨ Der all c-uses-Uberdeckungstest pr¨ ft offensichtlich lediglich Variablendeﬁnitionen, u die in berechnenden Zugriffen m¨ nden. Variablen, die ausschließlich pr¨ dikativ ver- u a ¨ wendet werden, werden somit nicht getestet. Der all c-uses/some p-uses-Uberde- ¨ ckungstest erweitert den all c-uses-Uberdeckungstest dahingehend, dass f¨ r aus- u schließlich pr¨ dikativ verwendete Variablen ebenfalls Testf¨ lle gefordert werden. a a Somit m¨ ssen die Testf¨ lle das folgende Kriterium erf¨ llen: u a u • F¨ r jeden Knoten vi im datenﬂussattributierten Kontrollﬂussgraph und jeder Va- u riablen x ∈ de f s(vi ) muss mindestens ein deﬁnitionsfreier Pfad bez¨ glich x von u Knoten vi zu jedem Knoten in dcu(x, vi ) getestet werden. • Ist dcu(x, vi ) leer, so muss mindestens ein deﬁnitionsfreier Pfad bez¨ glich x von u Knoten vi zu einer Kante in dpu(x, vi ) getestet werden.
7.2 Testfallgenerierung zur simulativen Eigenschaftspr¨ fung u 415 Beispiel 7.2.22. F¨ r das Programm aus Beispiel 7.2.16 fordert der all c-uses/some p- u uses-Uberdeckungstest die Testfalleingabe (vin , v1 , v2 , v3 , vout ). Die Deﬁnitionen in ¨ vin und v2 erfordern den Test der berechnenden Zugriffe in v2 und vout . Da damit bereits alle deﬁnierten Variablen getestet wurden, m¨ ssen keine weiteren Testf¨ lle u a hinzugenommen werden, obwohl der Zweig (v1 , v3 ) noch nicht getestet wurde. ¨ ¨ Der all c-uses/some p-uses-Uberdeckungstest subsumiert den all defs-Uberde- ckungstest. Er subsumiert aber weder den Zweig- noch den Anweisungs¨ berde- u ckungstest. ¨ all p-uses/some c-uses-Uberdeckungstest ¨ Analog zum all c-uses/some p-uses-Uberdeckungstest existiert der all p-uses/some c- ¨ uses-Uberdeckungstest. Bei diesem wird zus¨ tzlich zu den Testf¨ llen des all p-uses- a a ¨ Uberdeckungstests gefordert, dass f¨ r eine Variable, die ausschließlich berechnend u verwendet wird, also in keiner pr¨ dikativen Benutzung auftaucht, weitere Testf¨ lle a a generiert werden m¨ ssen. Das Kriterium f¨ r die Testf¨ lle lautet somit: u u a • F¨ r jeden Knoten vi im datenﬂussattributierten Kontrollﬂussgraph und jeder Va- u riablen x ∈ de f s(vi ) muss mindestens ein deﬁnitionsfreier Pfad bez¨ glich x von u Knoten vi zu jeder Kante in dpu(x, vi ) getestet werden. • Ist dpu(x, vi ) leer, so muss mindestens ein deﬁnitionsfreier Pfad bez¨ glich x von u Knoten vi zu einem Knoten in dcu(x, vi ) getestet werden. Beispiel 7.2.23. Betrachtet wird das Programm aus Beispiel 7.2.16 auf Seite 411. F¨ r u ¨ eine 100%-ige all p-uses/some c-uses-Uberdeckung sind die beiden Testfalleingaben (vin , v1 , v3 , vout ) und (vin , v1 , v2 , v3 , vout ) notwendig. Die Deﬁnitionen von min und max in vin erfordern den Test der pr¨ dikativen Verwendung in (v1 , v3 ) und (v1 , v2 ). a Zus¨ tzlich wird aber durch die Deﬁnitionen in Knoten v2 gefordert, dass der berech- a nende Zugriff in vout getestet wird. Dies ist allerdings bereits im zweiten Testfall enthalten. ¨ Der all p-uses/some c-uses-Uberdeckungstest subsumiert Zweig, Anweisungs- ¨ und all p-uses-Uberdeckungstest. ¨ all uses-Uberdeckungstest Die Kombination aus den all c-uses/some p-uses- und all p-uses/some c-uses-Uber- ¨ ¨ deckungstests f¨ hrt zu dem all uses-Uberdeckungstest. Es wird dabei gefordert, dass u f¨ r jede globale Deﬁnition jede erreichbare berechnende und pr¨ dikative Verwen- u a dung getestet wird. Das Kriterium f¨ r die Testf¨ lle lautet somit: F¨ r jeden Knoten vi u a u im datenﬂussattributierten Kontrollﬂussgraph und jeder Variablen x ∈ de f s(vi ) muss mindestens ein deﬁnitionsfreier Pfad bez¨ glich x von Knoten vi zu jedem Knoten u ¨ in dpu(x, vi ) und zu jeder Kante in dpu(x, vi ) getestet werden. Der all uses-Uber- deckungstest subsumiert somit den all c-uses/some p-uses- und den all p-uses/some ¨ c-uses-Uberdeckungstest. Die Subsumierungsrelationen der in diesem Abschnitt vorgestellten Verfahren zur Generierung strukturorientierter Testf¨ lle ist zusammenfassend in Abb. 7.20 dar- a gestellt.
416 7 Software-Veriﬁkation Pfad- ¨ uberdeckungstest strukturierter Mehrfach- all uses- Pfad- ¨ Bedingungs- Uberdeckungstest ¨ uberdeckungstest ¨ uberdeckungstest all c-uses/ all p-uses/ minimaler Mehrfach- some p-uses- some c-uses- Bedingungs- ¨ Uberdeckungstest ¨ Uberdeckungstest ¨ uberdeckungstest Bedingungs-/ all c-uses- all defs- all p-uses- ¨ ¨ ¨ Entscheidungs- Uberdeckungstest Uberdeckungstest Uberdeckungstest ¨ uberdeckungstest einfacher Zweig- Bedingungs- ¨ uberdeckungstest ¨ uberdeckungstest Anweisungs- ¨ uberdeckungstest Abb. 7.20. Subsumierungsrelation zwischen den Verfahren zur Generierung strukturorientier- ter Testf¨ lle a ¨ 7.3 Formale funktionale Eigenschaftsprufung von Programmen Die automatischen Verfahren zur formalen funktionalen Eigenschaftspr¨ fung von u Programmen haben in den vergangenen Jahren enorme Fortschritte verzeichnet. ¨ Einen guten Uberblick hier¨ ber gibt die Ver¨ ffentlichung [140]. Im Folgenden wer- u o den in Anlehnung an [140] einige Techniken n¨ her betrachtet. a 7.3.1 Statische Programmanalyse Der Begriff statische Programmanalyse beschreibt Techniken, mit deren Hilfe Infor- ¨ mationen uber das Verhalten von Programmen ermittelt werden k¨ nnen, ohne diese o auszuf¨ hren. Viele dieser Techniken wurden f¨ r die Optimierungsphase in Com- u u pilern konzipiert. Dennoch ist deren Anwendungsgebiet nicht auf diese Aufgabe beschr¨ nkt. Hier wird statische Programmanalyse im Kontext der formalen Eigen- a schaftspr¨ fung von Programmen betrachtet. u Ein grundlegendes Problem in der Programmveriﬁkation ist, dass viele Veriﬁka- tionsfragen unentscheidbar oder zu rechenintensiv sind, um sie zu beantworten. Des- halb berechnen Techniken zur statischen Programmanalyse typischerweise lediglich Approximationen f¨ r Eigenschaften. Diese m¨ ssen allerdings Korrektheitsgarantien u u liefern, d. h. nicht zu Fehlschl¨ ssen verleiten. u
7.3 Formale funktionale Eigenschaftspr¨ fung von Programmen u 417 Beispiel 7.3.1. Ein statisches Verfahren zur Detektion von Division durch Null“- ” Fehlern in einem gegeben Programm muss s¨ mtliche Werte eines Divisors, die zur a Laufzeit des Programms auftreten k¨ nnen, ber¨ cksichtigen. Da eine Aufz¨ hlung al- o u a ler potentiellen Werte in der Regel aus Zeitgr¨ nden nicht m¨ glich ist, arbeiten Ver- u o fahren zur statischen Programmanalyse typischerweise mit Teil- bzw. Obermengen. Verwendet die Analyse eine Teilmenge aller m¨ glichen Werte und ﬁndet dabei keine o ¨ Fehler, kann keine endg¨ ltige Aussage uber die Abwesenheit von Division durch u ” Null“-Fehlern gemacht werden. Liefert das Analyseverfahren dennoch dieses Ergeb- nis, so kann diese Aussage falsch sein, da die verwendet Approximation inkorrekt ist. Verwendet das Verfahren hingegen eine Obermenge aller m¨ glichen Werte eines o Divisors, so ist die Approximation korrekt, und die Aussage, dass keine Division ”¨ durch Null“-Fehlern existieren, gerechtfertigt. Allerdings kann eine solche Uberap- proximation zu falschnegativen Ergebnissen f¨ hren, d. h. der Fehler tritt lediglich u unter Verwendung von Werten auf, die zwar in der Obermenge, nicht aber in der ur- spr¨ nglichen Menge m¨ glicher Werte des Divisors liegt. In diesem Zusammenhang u o spricht man auch von unzul¨ ssigen Gegenbeispielen. a Im Gegensatz zu falschnegativen Ergebnissen k¨ nnen bei der statischen Pro- o grammanalyse auch falschpositive Ergebnisse auftreten. Hierbei handelt es sich um Testf¨ lle, die als fehlerfrei angesehen werden, es aber in Wirklichkeit gar nicht sind. a Aufgrund der Unentscheidbarkeit statischer Analyseprobleme kann nicht garantiert werden, dass eine Methode sowohl keine falschnegativen als auch keine falschposi- tiven Ergebnisse erzeugt. Statische Programmanalyse beruht auf der Idee der Fixpunktberechnung (siehe auch Anhang C.4). Dabei werden Wertemengen solange durch ein Programm pro- ¨ pagiert und angepasst, bis diese Mengen sich nicht weiter andern. Dies wird anhand des Beispiels aus [140] illustriert: Beispiel 7.3.2. Gegeben ist folgender Ausschnitt eines C-Programms: 1 int i = 0; 2 do { 3 assert(i
418 7 Software-Veriﬁkation CFG NOP 1. Iteration 2. Iteration INT v1 i = 0; i > 10 NOP {0} {0, 2} v2 i ≤ 10 {0} {0, 2} v3 NOP i = i + 2; i
7.3 Formale funktionale Eigenschaftspr¨ fung von Programmen u 419 da sich die dort ermittelte Wertemenge nicht ge¨ ndert hat. Die Menge {0, 2} a wird nun unver¨ ndert weiter an Knoten v3 propagiert. Dort werden die Elemente a um zwei erh¨ ht, weshalb sich f¨ r Zustand v4 die Wertemenge {2, 4} ergibt. Da o u beide Elemente echt kleiner f¨ nf sind, wird die Wertemenge nicht an v5 jedoch u aber an v2 propagiert. ¨ Die Iteration wird solange fortgesetzt, bis ein Fixpunkt erreicht ist, d. h. keine Ande- rungen in den Wertemengen auftreten. Die eben gerade beschriebene Programmanalyse wird als konkrete Interpretation bezeichnet. Dies liegt darin begr¨ ndet, dass Elemente aus INT und beliebigen Teil- u mengen daraus konkrete Werte und somit einen konkreten Wertebereich darstellen. Abstrakte Interpretation Konkrete Interpretation l¨ sst sich in der Praxis nicht anwenden, da die Wertemen- a gen schnell anwachsen. Bereits 1965 stellte Peter Naur fest, dass es ausreichend sein kann, abstrakte Werte bei der Programmanalyse zu verwenden [341]. Basierend auf diesem Ergebnis entwickelten Cousot und Cousot 1977 die Methode der abstrak- ten Interpretation [118]. Abstrakte Interpretation bedient sich zweier zentraler Kon- zepte: dem sog. abstrakten Wertebereich, der eine Approximation eines konkreten Wertebereichs ist, und sog. abstrakter Funktionen, die dazu dienen, konkrete Werte ¨ in abstrakte Werte zu ubersetzen. Abstrakte Interpretation hat zum Ziel, eine appro- ximative L¨ sung des Programmanalyseproblems zu liefern. Dabei wird das Verhal- o ten eines Programms f¨ r abstrakte Wertebereiche analysiert. Dies geschieht, indem u die Operationen auf den konkreten Wertebereichen aus der konkreten Interpretation durch geeignete Funktionen ersetzt werden. Abstrakte Wertebereiche lassen sich in relationale und nichtrelationale abstrak- te Wertebereiche einteilen. Beispiele f¨ r nichtrelationale Wertebereiche sind Vor- u zeichen-Wertebereiche, Intervall-Wertebereiche oder Kongruenz-Wertebereiche. Der Vorzeichen-Wertebereich besitzt drei Elemente {pos, neg, zero} zur Unterscheidung positiver und negativer Zahlen, sowie der Null. Intervall-Wertebereiche sind expres- siver, da der Vorzeichen-Wertebereich durch {[−∞, 0), [0, 0], (0, ∞]} repr¨ sentiert a werden kann. Beispiel 7.3.3. Betrachtet wird wiederum das Programmsegment aus Beispiel 7.3.2 mit dem Kontroll-Datenﬂussgraphen aus Abb. 7.21. Ein m¨ glicher abstrakter Werte- o bereich ist z. B. die Menge der Intervalle {[a, b] | a ≤ b∧a, b ∈ Z}. Die in der konkre- ten Interpretation verwendeten Operationen Addition und Vereinigung m¨ ssen f¨ r u u die abstrakte Interpretation ersetzt werden durch Addition und Vereinigung von In- tervallen. Die abstrakte Interpretation ist in Abb. 7.22 an dem Beispiel durchgef¨ hrt. u Im Folgenden seien min bzw. max der minimale bzw. maximale Wert, der sich im Wertebereich INT darstellen l¨ sst. In Zustand v1 , zu Beginn der ersten Iteration, a ist die Variable i noch nicht initialisiert und kann somit einen beliebigen Wert im Intervall [min, max] annehmen. Nach der Initialisierung (Zustand v2 ) besitzt i den
420 7 Software-Veriﬁkation CFG NOP 1. Iteration 2. Iteration 3. + 4. Iteration [min, max] v1 i = 0; i > 10 NOP [0, 0] [0, 2] [0, 4] v2 i ≤ 10 [0, 0] [0, 2] [0, 4] v3 NOP i = i + 2; i
7.3 Formale funktionale Eigenschaftspr¨ fung von Programmen u 421 ¨ Da es sich bei der Intervallbildung um eine Uberapproximation handelt, kann man auch f¨ r jede konkrete Programmausf¨ hrung schließen, dass die Zusicherung u u assert(x
422 7 Software-Veriﬁkation gezeigt werden kann. Dies ist nicht mit den oben beschriebenen relationalen abstrak- ten Wertebereichen m¨ glich. Der abstrakte Wertebereich der linearen Kongruenzen o verbindet Polyeder-Wertebereiche mit Kongruenz-Wertebereichen. Diese enthalten auch Gleichungen der Form a1 x1 + · · · + an xn = c mod k f¨ r ein gegebenes k. Damit u kann gezeigt werden, dass (2 · x + 1) mod k ungleich y mod k ist, was auch die Frage nach einer m¨ glichen Division durch Null beantwortet. o ¨ 7.3.2 SAT-basierte Modellprufung von C-Programmen F¨ r die SAT-basierte Modellpr¨ fung (siehe Abschnitt 5.3.2) wird, neben der zu u u pr¨ fenden Eigenschaft, ein Modell des Programms ben¨ tigt. Dieses muss ein end- u o licher Automat sein, der aus Zust¨ nden und Zustands¨ berg¨ ngen besteht. In einem a u a Programm fasst ein Zustand den Wert des Programmz¨ hlers, die Werte der Pro- a grammvariablen und den Zustand des Speichers zusammen. Zustands¨ berg¨ nge be- u a o ¨ schreiben m¨ gliche Anderungen bei der Programmausf¨ hrung von einem Zustand u zum n¨ chsten. a Da der Kontrollﬂuss lediglich am Ende eines Grundblocks verzweigen und am Anfang eines Grundblocks eintreten kann, kann es sinnvoll sein, anstatt jede An- weisung einzeln zu codieren, eine Codierung auf Grundbl¨ cken vorzunehmen. Ein o solches Verfahren ist in [242] beschrieben. Beispiel 7.3.6. Gegeben ist das folgende C-Programm [242]: 1 void func1() { 2 int x = 3; 3 int y = x - 3; 4 while (x 6) 14 t -= 3; 15 else 16 t--; 17 return t; 18 } Der resultierende Kontroll-Datenﬂussgraph ist in Abb. 7.23 zu sehen. Man erkennt, dass jeder Zustand vi im Kontrollﬂussgraphen einem Grundblock im Programm ent- spricht. Außerdem ist gezeigt, wie Parameter im Falle nichtrekursiver Funktions- ¨ ¨ aufrufe ubergeben werden. Dabei werden Argumente in der Variable l ubergeben
7.3 Formale funktionale Eigenschaftspr¨ fung von Programmen u 423 und mittels der Variablen r wird unterschieden, an welche Variable das Ergebnis zu ¨ ubertragen ist. NOP NOP y++; x = 3; y = 0; v1 NOP NOP v2 NOP NOP x>4 x≤4 v3 l = x; r = 0; l = y; r = 1; v4 v5 NOP NOP v6 NOP NOP t >6 t ≤6 NOP v7 v8 t = l + 2; t -= 3; t--; v9 NOP NOP r=0 r=1 NOP NOP v10 v11 NOP x = t; y = t; NOP NOP Abb. 7.23. Kontroll-Datenﬂussgraph f¨ r das Programm aus Beispiel 7.3.6 u Jedem Grundblock i (Zustand im Kontrollﬂussgraphen) wird nun eine einzel- ne bin¨ re Variable bi ∈ B zugeordnet, die anzeigt, ob der Kontrollﬂuss gerade in a diesem Grundblock liegt. Die Belegung der Variablen bi kann direkt aus dem Pro- grammz¨ hler abgeleitet werden. Man beachte, dass bi = T impliziert, dass ∀ j=i b j = a F ist. Nach der Konstruktion des Kontroll-Datenﬂussgraphen werden zun¨ chst die Da- a tenﬂussgraphen zu jedem Basisblock einzeln in Booleschen Formeln codiert. Dabei wird f¨ r jede Zuweisung var = expr eine kombinatorische Schaltung f¨ r expr er- u u
424 7 Software-Veriﬁkation stellt, welche sich direkt als Boolesche Funktionen darstellen l¨ sst. Eine Addition a wird beispielsweise durch einen Ripple-Carry-Addierer ersetzt. Der Ausdruck Vik bezeichne dann die Zuweisung an die Variable vari im Grundblock k. Die Codie- rung aller Grundbl¨ cke resultiert darin, dass alle Variablen durch endliche Bitbreiten o repr¨ sentiert werden. Diese Bitbreiten ergeben sich aus der Mikroarchitektur des ver- a wendeten Prozessors. Zum Aufstellen der Zustands¨ bergangsrelation R wird nun f¨ r jede Variable vari u u der Folgezustand vari berechnet. Unter der Annahme, dass es n Grundbl¨ cke gibt o und die Variable vari in den Grundbl¨ cken 1, . . . , m Werte zugewiesen bekommt o (m ≤ n) und in den Bl¨ cken m + 1, . . . , n nicht geschrieben wird, kann dies durch o folgenden Ausdruck erfolgen: m n vari = b j ∧Vi j ∨ b j ∧ vari j=1 j=m+1 F¨ r die SAT-basierte Modellpr¨ fung muss die Zustands¨ bergangsrelation abge- u u u ¨ rollt werden. Wird die Ubergangsrelation k mal abgerollt, so ist die resultierende Boolesche Funktion um den Faktor k gr¨ ßer. F¨ r große Programme verbietet sich o u ein solches Vorgehen, wie das folgende Beispiel aus [140] zeigt. Beispiel 7.3.7. Abbildung 7.24a) zeigt den Kontrollﬂussgraphen eines Programms. Jeder Knoten entspricht einem Basisblock und die Kanten zeigen den m¨ glichen o Kontrollﬂuss an, wobei die Bedingungen nicht dargestellt sind. In Abb. 7.24b) ist der 6-fach abgerollte Kontrollﬂussgraph zu sehen. Man beachte, dass v1 lediglich in Schritt 0 zu erreichen ist. Weiterhin ist v2 nur zu den Zeitschritten 1, 3, 5 erreichbar. Zustandsraumreduktion durch Schleifenabwicklung In Beispiel 7.3.7 wurde gezeigt, dass k-faches Abrollen des Kontrollﬂussgraphen in einem Zustandsraum resultiert, der viele unerreichbare Zust¨ nde enth¨ lt. Eine wich- a a tige Beobachtung in diesem Zusammenhang ist, dass v1 , v4 und v5 auf jedem Pfad maximal einmal durchlaufen werden. Dennoch sind in Abb. 7.24b) drei erreichbare Instanzen von v4 und v5 zu sehen. Eine solche Redundanz kann verhindert werden. ¨ Die grundlegende Idee ist, dass nicht die gesamte Ubergangsrelation abgerollt, sondern Schleifen separat abgewickelt werden. Syntaktisch bedeutet dies, dass der Schleifenrumpf repliziert wird und der urspr¨ ngliche Kontrollﬂuss durch geeignete u W¨ chterfunktionen erhalten bleibt. a Beispiel 7.3.8. Gegeben ist die folgende Schleife: 1 while(x) 2 body(); Eine zweifache Schleifenabwicklung sieht dann wie folgt aus: 1 if(x) { 2 body(); 3 if(x) 4 body();
7.3 Formale funktionale Eigenschaftspr¨ fung von Programmen u 425 a) b) k c) k 0 v1 v2 v3 v4 v5 0 v1 v1 1 v1 v2 v3 v4 v5 1 v2 v2 2 v1 v2 v3 v4 v5 2 v3 v3 3 v1 v2 v3 v4 v5 3 v2 v4 4 v1 v2 v3 v4 v5 4 v3 v5 5 v1 v2 v3 v4 v5 5 v4 6 v1 v2 v3 v4 v5 6 v5 Abb. 7.24. a) Kontrollﬂussgraph, b) f¨ r k = 6 abgerollter Kontrollﬂussgraph und c) Kontroll- u ﬂussgraph mit abgewickelter Schleife [140] 5 else 6 assert(false); 7 } F¨ r das Programm aus Beispiel 7.3.7 kann der Effekt einer zweifachen Schlei- u fenabwicklung in Abb. 7.24c) gesehen werden. Der abgerollte Kontrollﬂussgraph ist deutlich kompakter als der in Abb. 7.24b) dargestellte Kontrollﬂussgraph, der sich ¨ durch Abrollen der Ubergangsrelation ergibt. Der Nachteil ist allerdings, dass durch die Schleifenabwicklung mehr Evaluierungsschritte ben¨ tigt werden k¨ nnen, um o o einen gesuchten Zustand zu erreichen. In Abb. 7.24b) erkennt man nach dem Abrol- len von einem Zeitschritt, dass der Zustand v4 erreichbar ist, w¨ hrend in Abb. 7.24c) a hierzu f¨ nf Zeitschritte ben¨ tigt werden. u o ¨ 7.3.3 Modellprufung durch Abstraktionsverfeinerung Die Unterscheidung von statischer Programmanalyse und Modellpr¨ fung ist his- u torisch entstanden. W¨ hrend die statische Programmanalyse von Beginn an die a ¨ Uberpr¨ fung einfacher Tatsachen in Programmen zum Ziel hatte, wurden Modell- u u ¨ pr¨ fungsverfahren zur Uberpr¨ fung temporallogischer Aussagen auf endlichen Au- u tomaten entwickelt. Aufgrund der praktischeren Zielsetzung entwickelten sich die Methoden zur statischen Programmanalyse schnell in Richtung Abstraktionstechni- ken. Dahingegen blieb die Modellpr¨ fung jahrelang eine Technik, die exakte Ergeb- u ¨ nisse ohne Uberapproximationen liefert. Mittlerweile unterst¨ tzen Werkzeuge zur u
426 7 Software-Veriﬁkation statischen Programmanalyse auch komplexe Formeln als Speziﬁkation zu pr¨ fender u funktionaler Eigenschaften und Verfahren zur Modellpr¨ fung von Programmen inte- u grieren Abstraktionstechniken. Somit verschwindet die Grenze zwischen statischer Programmanalyse und Modellpr¨ fung zunehmend. u F¨ r die SAT-basierte Modellpr¨ fung von Programmen muss das Programm u u ¨ zun¨ chst in eine Boolesche Formel ubersetzt werden. Dies kann wie im vorheri- a gen Abschnitt 7.3.2 vorgenommen werden, wobei der Programmz¨ hler, die globa- a len Variablen und die Speicherbelegung den Zustand des Programms bilden. Da der Zustandsraum eines Programms durch die Verwendung von komplexen Datentypen sehr groß sein kann, muss man typischerweise bei der Erstellung des Programm- modells davon abstrahieren. Die heutzutage wichtigste Technik daf¨ r ist die sog. u Pr¨ dikatenabstraktion. Die Wahl geeigneter Pr¨ dikate ist bei der Pr¨ dikatenabstrak- a a a tion die zentrale Herausforderung. Ein Verfahren, welches auf Abstraktionsverfeine- rung beruht, wurde von Clarke et al. [100] vorgeschlagen und ist unter dem Namen CEGAR (engl. CounterExample-Guided Abstraction Reﬁnement) bekannt geworden. Die prinzipielle Idee des Verfahrens ist in Abb. 7.25 zu sehen. C-Programm Abstraktion Modellpr¨ fung u Ja Eigenschaft fehlerfrei? erf¨ llt u Nein Simulation Nein Ja berichte Verfeinerung zul¨ ssig? a Gegenbeispiel Abb. 7.25. Eine durch Gegenbeispiele gesteuerte Abstraktionsverfeinerung Die Abstraktionsverfeinerung wird dabei durch Gegenbeispiele, die ein Modell- pr¨ fungsverfahren liefert, gesteuert. Dabei wird in einem ersten Schritt eine Pr¨ di- u a katenabstraktion des C-Programms bestimmt. Anschließend wird das Modell dahin- ¨ gehend uberpr¨ ft, ob es die zu pr¨ fende Eigenschaft erf¨ llt. Ist dies der Fall, ist die u u u Modellpr¨ fung erfolgreich abgeschlossen, d. h. das C-Programm erf¨ llt die gefor- u u derte Eigenschaft. Liefert die Modellpr¨ fung jedoch ein negatives Ergebnis, muss u a u ¨ zun¨ chst gepr¨ ft werden, ob das gefundene Gegenbeispiel uberhaupt einem zul¨ ssi- a gen Berechnungspfad im C-Programm entspricht. Dies ist notwendig, da durch die
7.3 Formale funktionale Eigenschaftspr¨ fung von Programmen u 427 ¨ ¨ Uberapproximation falschnegative Ergebnisse entstehen k¨ nnen. Die Uberpr¨ fung o u kann beispielsweise durch die Simulation des Gegenbeispiels mit dem Programm erfolgen. Ist das gefundene Gegenbeispiel zul¨ ssig, kann es mit dem C-Programm a reproduziert werden. Somit wurde ein echtes Gegenbeispiel gefunden und das C- Programm erf¨ llt die geforderte Eigenschaft nicht. Ist das Gegenbeispiel hingegen u nicht zul¨ ssig, muss verhindert werden, dass die Modellpr¨ fung in einer weiteren a u Iteration den gleichen Fehler im abstrakten Modell ﬁndet, der ja im konkreten Pro- ¨ gramm nicht vorliegt. Dies erfolgt dadurch, dass die Uberapproximation verfeinert wird. Die Abstraktionsverfeinerung im CEGAR-Ansatz l¨ uft also iterativ in vier Schrit- a ten ab: Abstraktion, Modellpr¨ fung, Simulation und Verfeinerung. Diese Schritte u werden im Folgenden n¨ her diskutiert (siehe auch [140]): a Abstraktion C-Programme bestehen aus Sequenzen von Anweisungen i1 , i2 , . . . . Durch die Ausf¨ hrung einer Instruktion i wird der momentane Programmzustand in einen Fol- u ¨ gezustand uberf¨ hrt. Dies wird durch die Relation Ri beschrieben, die f¨ r Programm- u u zust¨ nde Folgezust¨ nde, die aus der Ausf¨ hrung von i resultieren, bestimmt. Die a a u ¨ Vereinigung aller Relationen Ri ist die Ubergangsrelation R des Programms, welche die Grundlage f¨ r die Modellpr¨ fung bildet. u u u ¨ Da f¨ r reale Programme die Ubergangsrelation R zu komplex werden w¨ rde, u a ˆ muss zun¨ chst eine Abstraktion R bestimmt werden. Dies kann mittels Pr¨ dikaten- a ¨ abstraktion erfolgen, wobei Pr¨ dikate uber Programmvariablen gebildet werden. Da- a bei bipartitioniert ein Pr¨ dikat p die Zustandsmenge des Programms in Zust¨ nde, in a a denen p = T ist, und Zust¨ nde, in denen p = F gilt. Durch Verwendung mehrerer a Pr¨ dikate werden die Partitionen weiter unterteilt. Jede Partition bildet dann einen a abstrakten Zustand. Werden also n Pr¨ dikate gebildet, so wird der Zustandsraum a in 2n abstrakte Zust¨ nde partitioniert. Jeder abstrakte Zustand entspricht dann einer a der 2n m¨ glichen Variablenbelegungen. Dieses Vorgehen entspricht dem der funktio- o ¨ nalen Aquivalenzklassenbildung zur funktionsorientierten Testfallgenerierung (siehe Abschnitt 7.2.1). Seien s0 und s1 abstrakte Zust¨ nde. Es gilt dann: Es gibt einen Zustands¨ bergang ˆ ˆ a u ˆ in R, wenn es konkrete Zust¨ nde s0 und s1 in den zugeh¨ rigen Partitionen gibt, die a o durch einen Zustands¨ bergang miteinander verbunden sind, d. h. u (s0 , s1 ) ∈ R ⇒ ∃s0 ∈ s0 , s1 ∈ s1 : (s0 , s1 ) ∈ R . ˆ ˆ ˆ ˆ ˆ Dies wird als existentielle Abstraktion bezeichnet, die korrekte Abstraktionen f¨ r Er- u reichbarkeitsanalysen liefert [101]. Das resultierende abstrakte Programm, welches ˆ sich aus R ergibt, wird durch ein sog. Boolesches Programm repr¨ sentiert [27]. Die- a ses Boolesche Programm besitzt die selben Kontrollanweisungen wie das originale C-Programm, allerdings sind alle verwendeten Variablen nun bin¨ r.a ¨ Beispiel 7.3.9. Betrachtet wird ein Programm ahnlich wie in Beispiel 7.3.2. In Zeile 4 ist das Inkrement um 2 durch ein Inkrement um 1 ersetzt. Das neue Programm sieht
428 7 Software-Veriﬁkation somit wie folgt aus: 1 int i = 0; 2 do { 3 assert(i 10 NOP v2 i ≤ 10 v3 NOP i = i + 1; i 10 ist, muss in diesem Fall b1 zwingend gleich F sein. Der Fall i ≤ 10 schließt auch i = 0 ein, was zur Folge hat, dass die Bedingung zur Konstanten T wird, also uberhaupt nicht von b1 abh¨ ngt. Die ¨ a Pr¨ dikatenabstraktion f¨ r die Konditionale in der Verzweigung in Zustand v4 werden a u auf die gleiche Art bestimmt. Die Berechnung des Inkrements im Zustand v3 muss nun ebenfalls nur mit b1 erfolgen. Besitzt die Variable i bei Erreichen der Inkrement-Anweisung den Wert 0
7.3 Formale funktionale Eigenschaftspr¨ fung von Programmen u 429 a) b) CFG CFG NOP NOP v1 v1 b1 := T b1 := T b2 := T b1 = F NOP b2 = F NOP v2 v2 T T v3 NOP v3 NOP b1, b2 := b1 := b1 ? F : − b1 ? F : (b2 ? − : F), T b2 = T b2 ? (b1 ? T : −) : F) v4 v4 b1 = F NOP b2 = F NOP v5 ve v5 ve Abb. 7.27. Kontroll-Datenﬂussgraphen f¨ r die Pr¨ dikatenabstraktion a) i = 0 und b) i = 0 und u a i
430 7 Software-Veriﬁkation Bei Verwendung von n Pr¨ dikaten ergeben sich 2n abstrakte Zust¨ nde und es a a werden (2n )2 Schritte ben¨ tigt, um die Abstraktion zu berechnen. o Modellpr¨ fung u Die Modellpr¨ fungsphase ist oftmals der Flaschenhals in der auf Pr¨ dikatenabstrak- u a tion basierenden Veriﬁkation. Der Grund hierf¨ r ist, dass SAT-basierte Verfahren zur u Modellpr¨ fung im Allgemeinen nicht geeignet sind, um Fixpunkte zu detektieren u (siehe auch Abschnitt 5.3.2). Deshalb m¨ ssen BDD-basierte Verfahren zum Einsatz u kommen, die aufgrund des exponentiellen Speicherbedarfs nicht skalieren und f¨ r u realistische Systeme im Allgemeinen nicht anwendbar sind. Eine Alternative stellen sog. QBF-Solver (quantiﬁzierte Boolesche Funktionen) dar. Diese haben allerdings ¨ ahnliche Probleme wie BDD-basierte Verfahren. Ohne diese Problematik weiter zu vertiefen, wird anhand eines Beispiels [140] illustriert, wie die Erreichbarkeitsanalyse durchgef¨ hrt werden kann. u Beispiel 7.3.10. Betrachtet wird der Kontroll-Datenﬂussgraph aus Abb. 7.27b). Nach dem ersten Zustands¨ bergang von v1 nach v2 sind beide Variablen b1 und b2 mit dem u Wert T belegt. Die symbolische Repr¨ sentation des Programmzustands lautet somit a b1 ∧ b2 . Nach Erreichen des Zustands v4 ist der abstrakte Zustand gegeben durch ¬b1 ∧ b2 . Durch das Zur¨ ckpropagieren zu Zustand v2 ergibt sich nun f¨ r v2 der u u Zustand (b1 ∧ b2 ) ∨ (¬b1 ∧ b2 ). Durch Anwendung der Absorptionsregel ergibt dies ¨ den abstrakten Zustand b2 . Bei einer weiteren Iteration wird uber die Zust¨ nde v2 a und v3 somit der Zustand T in v4 erreicht. Davon werden aber lediglich (b1 ∧ b2 ) ∨ (¬b1 ∧b2 ) an v2 und (b1 ∧¬b2 )∨(¬b1 ∧¬b2 ) an v5 propagiert. Dies ist offensichtlich ein Fixpunkt in der Erreichbarkeitsanalyse. Interessant ist in diesem Zusammenhang, dass das Erreichbarkeitsproblem von Booleschen Programmen entscheidbar ist, und zwar, obwohl der Programmstack po- tentiell unendlich groß ist. Die Erkl¨ rung ist, dass f¨ r einen gegeben Zustand der a u resultierende Folgezustand aus dem obersten Element auf dem Stack und der Bele- gung der globalen Variablen folgt, was als endliche Menge darstellbar ist. Simulation Findet die Erreichbarkeitsanalyse einen Pfad vom abstrakten Anfangszustand zu ei- ¨ nem abstrakten Zustand, der einen Fehlerfall darstellt, so muss uberpr¨ ft werden, u ob es sich bei diesem Pfad um ein zul¨ ssiges Gegenbeispiel handelt. Dies bedeu- a ¨ tet, es muss uberpr¨ ft werden, ob eine konkrete Testfalleingabe f¨ r das C-Programm u u existiert, so dass vom konkreten Anfangszustand ein Fehlerzustand erreichbar ist. Da eine konkrete Testfalleingabe gesucht wird, spricht man auch von der Simulation des Programms. Beispiel 7.3.11. In Abb. 7.27a) ist der Fehlerzustand ve uber den Pfad v1 , v2 , v3 , v4 , ¨ v2 , ve erreichbar. Die verwendete Abstraktion ist in diesem Fall durch das einzelne Pr¨ dikat i = 0 gegeben. Dieses Gegenbeispiel ist allerdings nicht zul¨ ssig, da der a a Wert der Variable i in der Simulation beim zweiten Erreichen von v2 den Wert 1
7.4 Zeitanalyse 431 a ¨ tr¨ gt und somit kein Ubergang in den Zustand ve m¨ glich ist. F¨ r einen solchen o u Ubergang m¨ sste die Bedingung i > 10 erf¨ llt sein. ¨ u u Die Erkennung unzul¨ ssiger Gegenbeispiele verlangt nach einer Verfeinerung a des abstrakten Modells, so dass dieses unzul¨ ssige Gegenbeispiel in einem folgenden a Veriﬁkationsschritt nicht wieder auftreten kann. Verfeinerung Ein Grund f¨ r die Entstehung unzul¨ ssiger Gegenbeispiele besteht darin, dass die u a gew¨ hlte Pr¨ dikatenmenge nicht aussagekr¨ ftig genug gew¨ hlt wurde. Dieses Pro- a a a a blem kann durch Hinzunahme weiterer Pr¨ dikate gel¨ st werden. Das folgende Bei- a o spiel stammt wiederum aus [140]. Beispiel 7.3.12. Das unzul¨ ssige Gegenbeispiel in Beispiel 7.3.11 f¨ hrte zu der a u Ausf¨ hrungssequenz i = 0, [i ≤ 10], i + +, [i < 5], [i > 10] . Hierf¨ r k¨ nnen die u u o sog. schw¨ chste Vorbedingung und die st¨ rkste Nachbedingung bestimmt werden. a a Die schw¨ chste Vorbedingung ist die schw¨ chste aller m¨ glichen Bedingungen, die a a o vor Beginn der Ausf¨ hrung der Sequenz gelten m¨ ssen, so dass (i < 5) ∧ (i > 10) u u nach Ausf¨ hrung der Sequenz gilt. In diesem Fall ist dies (i < 5) ∧ (i > 10). Die u st¨ rkste Nachbedingung ist die st¨ rkste aller m¨ glichen Bedingungen, die nach a a o Ausf¨ hrung der Sequenz gelten muss, so dass vor Ausf¨ hrung der Sequenz die Be- u u dingung (i = 0) ∧ (i ≤ 10) gilt. Dies ist (i = 1) ∧ (i ≥ 5). Sowohl die schw¨ chste a Vorbedingung als auch die st¨ rkste Nachbedingung sind inkonsistent und somit ein a Beweis, dass das abstrakte Gegenbeispiel unzul¨ ssig ist. F¨ r die Verfeinerung ist es a u nun beispielsweise ausreichend, die neuen Pr¨ dikate i = 1 und i < 5 mit aufzuneh- a men, um dieses Gegenbeispiel von zuk¨ nftigen Veriﬁkationsphasen auszuschließen. u Wie Abb. 7.27b) zeigt, ist die Abstraktionsverfeinerung mit dem Pr¨ dikat i < 5 a hinreichend, um das Nichterreichen von ve im resultierenden Booleschen Programm zu zeigen. In der Tat w¨ re es sogar ausreichend gewesen, nur i < 5 als Pr¨ dikat von a a Beginn an zu verwenden, was zu einer korrekten Abstraktion gef¨ hrt h¨ tte. u a Man sieht also, dass die Auswahl geeigneter Pr¨ dikate durchaus nicht leicht ist. a Aus diesem Grund werden heutzutage im Wesentlichen Heuristiken verwendet, um m¨ glichst kleine Pr¨ dikatenmengen zu generieren, die ein Gegenbeispiel erkl¨ ren. o a a 7.4 Zeitanalyse F¨ r die nichtfunktionale Eigenschaftspr¨ fung von Zeitaspekten der Software wird, u u wie im Fall der Hardware-Veriﬁkation, davon ausgegangen, dass das Problem zwei- stuﬁg ist, d. h., dass zun¨ chst das Zeitverhalten der Software analysiert und die Er- a gebnisse dieser Zeitanalyse mit den nichtfunktionalen Anforderungen der Speziﬁka- tion verglichen werden. Auf Modulebene liegen diese Anforderungen typischerweise als sog. engl. Deadlines f¨ r einzelne Software-Prozesse vor. Dabei speziﬁziert eine u Deadline die maximale Zeitspanne von Aktivierung eines Prozesses bis zu dessen
432 7 Software-Veriﬁkation Abarbeitung (Beendigung). Eine Zeitanalyse auf Modulebene hat somit die Aufga- be, f¨ r alle Prozesse die maximalen Zeitspannen von deren Aktivierung bis deren u Beendigung, unter Ber¨ cksichtigung von m¨ glichen Unterbrechungen durch andere u o ¨ Prozesse, zu bestimmen. Da es sich hierbei um die Uberpr¨ fung von Echtzeitanfor- u derungen handelt, spricht man auch von Echtzeitanalyse. Zur Durchf¨ hrung der Echtzeitanalyse ist es aber notwendig, neben den Unter- u brechungszeiten durch andere Prozesse, die Ausf¨ hrungszeit jedes Prozesses auf u dem Prozessor zu kennen f¨ r den Fall, dass der Prozess nicht unterbrochen wird. u Diese Zeiten werden als engl. Core Executiuon Times (CET) bezeichnet. Man un- terscheidet zwischen einer k¨ rzesten (engl. Best Case Execution Time, BCET) und u einer l¨ ngsten Ausf¨ hrungszeit (engl. Worst Case Execution Time, WCET). Sowohl a u BCETs als auch WCETs von Prozessen h¨ ngen vom Kontrollﬂuss des Prozesses, a der Mikroarchitektur und dem Anfangszustand des verwendeten Prozessors sowie der Eingabe ab. Im Folgenden werden zun¨ chst Verfahren zur BCET- und WCET-Analyse vor- a gestellt. Anschließend erfolgt eine Einf¨ hrung in Echtzeitanalysemethoden auf Mo- u dulebene. 7.4.1 BCET- und WCET-Analyse F¨ r die Zeitanalyse auf h¨ heren Abstraktionsebenen ist es notwendig, die Ausf¨ h- u o u rungszeiten aller Prozesse zu kennen. Genauer formuliert, m¨ ssen die k¨ rzesten u u (engl. Best Case Execution Times, BCET) und die l¨ ngsten Ausf¨ hrungszeiten (engl. a u Worst Case Execution Time, WCET) jedes Prozesses auf dem gegebenen Prozessor unter der Annahme bekannt sein, dass der Prozess nicht unterbrochen oder blockiert wird. Diese Zeiten h¨ ngen von verschiedenen Faktoren ab: Zum einen vom Kontroll- a ﬂuss des Prozesses sowie den Eingabedaten, zum anderen ist die Mikroarchitektur und der Anfangszustand des Prozessors (inklusive Cache) entscheidend. Abbildung 7.28 zeigt eine Verteilung der Ausf¨ hrungszeit eines Prozesses. Die u k¨ rzeste Ausf¨ hrungszeit ist die BCET, w¨ hrend die l¨ ngste Ausf¨ hrungszeit die u u a a u WCET ist. Verfahren zur Bestimmung von BCET und WCET eines Prozesses k¨ nnen simulativ oder formal sein. Stand der Technik im industriellen Umfeld o sind simulative Methoden, zu denen auch messbasierte Verfahren z¨ hlen. Die Si- a mulation verwendet eine Reihe von Stimuli, um BCET und WCET eines Prozes- se zu bestimmen. Das Ergebnis ist aber im Allgemeinen eine kleinste beobachtete u ¨ Ausf¨ hrungszeit, die eine Uberapproximation der BCET ist, und eine gr¨ ßte beob- o achtete Ausf¨ hrungszeit, die eine Unterapproximation der WCET ist. Aufgrund der u Unvollst¨ ndigkeit simulativer Methoden sind diese im Allgemeinen nicht f¨ r das Ve- a u riﬁkationsziel des Beweises geeignet, wie in Abb. 7.28 zu sehen ist. F¨ r die Anwendung formaler Zeitanalysemethoden muss aufgrund der hohen Re- u chenzeit eine Abstraktion des Systems betrachtet werden. Aus diesem Grund erh¨ lt a man bei Einsatz formaler Methoden untere und obere Zeitschranken. Diese m¨ ssen u einerseits sicher sein, d. h. sie d¨ rfen zu keinen falschpositiven Ergebnissen der Ei- u genschaftspr¨ fung f¨ hren, wie im Fall der simulativen Analyse, andererseits m¨ ssen u u u
7.4 Zeitanalyse 433 Verteilung der Ausf¨ hrungszeit kleinste beobachtete obere Zeitschranke untere Zeitschranke gr¨ ßte beobachtete u Ausf¨ hrungszeit Ausf¨ hrungszeit WCET BCET u u o 0 gemessene Ausf¨ hrungszeit u t m¨ gliche Ausf¨ hrungszeit o u Ergebnis der Zeitanalyse Abb. 7.28. Verteilungsfunktion der Ausf¨ hrungszeiten eines Prozesses [464] u diese Schranken m¨ glichst genau BCET und WCET widerspiegeln, um falschnega- o tive Ergebnisse bei der Veriﬁkation des Zeitverhaltens zu vermeiden. Im Folgenden wird die formale BCET/WCET-Analyse vorgestellt. Da BCET und WCET eines Prozesses von dessen Kontrollﬂuss und den Ein- gabedaten sowie der Mikroarchitektur und -zustand abh¨ ngen, kann die formale a BCET/WCET-Analyse in zwei Teilprobleme aufgeteilt werden: 1. Programmpfadanalyse: Zum einen muss bestimmt werden, welcher Ausf¨ h- u rungspfad, und somit welche Eingabedaten, zu einer schnellsten bzw. langsams- ten Ausf¨ hrung eines Prozesses f¨ hren. Der Ausf¨ hrungspfad ist dann eine Se- u u u quenz an Instruktionen, die durchlaufen werden. 2. Modellierung der Zielarchitektur: Architekturmerkmale, die Einﬂuss auf das Zeitverhalten der Pfadausf¨ hrung haben, m¨ ssen ber¨ cksichtigt werden. Zu die- u u u sen Merkmalen z¨ hlen Pipelines, Caches, spekulative Instruktionsausf¨ hrung a u etc. Weiterhin hat der Zustand, in dem sich der Prozessor beﬁndet, einen ent- scheidenden Einﬂuss auf die Ausf¨ hrungszeit. Der Zustand muss betrachtet wer- u den, da mehrere Prozesse auf ein und dem selben Prozessor ausgef¨ hrt werden u k¨ nnen. o Diese beiden Probleme sind voneinander abh¨ ngig, d. h. es gibt nicht zwangsl¨ uﬁg a a einen Ausf¨ hrungspfad f¨ r den Prozess, der f¨ r alle m¨ glichen Mikroarchitekturen u u u o und Zust¨ nden die schnellste bzw. langsamste Ausf¨ hrungszeit liefert. a u Programmpfadanalyse Zun¨ chst wird die WCET-Analyse unabh¨ ngig von der Architekturmodellierung vor- a a gestellt. Aufgabe der Programmpfadanalyse ist es, zu bestimmen, welche Ausf¨ h- u