Digitale Hardware/ Software-Systeme- P18

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

Thêm vào BST

Báo xấu

53
lượt xem 4
download

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

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

504 8 Systemveriﬁkation periodischen Ereignisstrom darstellen. Allerdings kann durch Pufferung und peri- odische Wiedergabe von Ereignissen eine rein periodischer Ereignisstrom aus einem periodischen Ereignisstrom mit Jitter konstruiert werden. Hierzu ist die Ermittlung der Ereignisadaptierungsfunktion (EAF) notwendig (siehe Abb. 8.29c)). Die Ermitt- lung der EAF erfolgt auf Basis des Ereignismodells f¨ r den Ausgabeereignisstrom u und dem Ereignismodell f¨ r den Eingabeereignisstrom. u F¨ r das Beispiel aus Abb. 8.29c) (X = (PX , JX ) und Y = (PY )) kann ein Puffer u der Gr¨ ße nEAF := 1 verwendet werden und die Periode PY auf PX gesetzt werden. o + Die Verz¨ gerungszeit eines Ereignisses betr¨ gt dann dEAF = PX Zeiteinheiten. Etwas o a komplizierter ist der Fall f¨ r die Umwandlung eines periodischen Ereignisstroms mit u Bursts (X = (PX , dX , bX )) in einen rein periodischen Ereignisstrom (Y = (PY )). Mit dem Wissen, dass maximal bX Ereignisse in einer Zeitspanne von PX Zeiteinheiten auftreten k¨ nnen, kann PY zu PY := PX bestimmt werden. Die maximale Verz¨ gerung o bX o eines Ereignisses betr¨ gt: a + dEAF = PX − (bX − 1) · dX (8.4) Dies wird anhand eines Beispiels aus [378] verdeutlicht: Beispiel 8.2.5. Gegeben ist das Ereignismodell eines periodischen Ausgabeereig- nisstroms mit Periode PX und minimaler Ankunftszeit dX . Die maximale Anzahl an Ereignissen in einer Periode PX ist bX := 5. Hieraus ergibt sich die Periode PY zu PY = PX . Abbildung 8.31 zeigt die maximale Verz¨ gerung eines Ereignisses als 5 o grauen Kasten. Diese ergibt sich f¨ r das letzte Ereignis eines Bursts. u dX X Y 0 PY 2PY 3PY 5PY = PX τ Abb. 8.31. Maximale Verz¨ gerungszeit f¨ r ein Ereignis o u Da die Ereignisse periodisch aus dem Puffer entnommen werden, l¨ sst sich die ma- a ximale Anzahl n+ an Ereignissen in dem Puffer bestimmen zu: EAF + dEAF PX − (bX − 1) · dX n+ = EAF = PX PY bX dX = bX − bx · (bx − 1) · (8.5) PX F¨ r die Umwandlung von Ereignisstr¨ men mit Adaptierung aus Abb. 8.30 sind u o die Puffergr¨ ßen nEAF , die Perioden PEAF und die maximalen Verz¨ gerungszeiten o o
8.2 Zeitanalyse auf Systemebene 505 + dEAF f¨ r die jeweiligen Ereignisadaptierungsfunktionen sowie die Ereignismodell- u schnittstelle in Tabelle 8.2 angegeben. Man erkennt, dass die Ereignisadaptierungs- funktion lediglich von dem Ausgabeereignisstrom X abh¨ ngt, was an der Verwen- a dung periodischer Adpatierungsfunktionen liegt. Tabelle 8.2. Ereignisadaptierungsfunktionen und Ereignismodellschnittstellen f¨ r die Um- u wandlung von Ereignisstr¨ men mit Adaptierung nach Abb. 8.30 [378] o + X →Y EMIFX→Y PEAF nEAF dEAF (PX , JX ) → (PY ) PY := PEAF PX 1 PX (PX , JX ) → (PY , dY , bY ) PY := PEAF , dY := PY , bY := 1 PX 1 PX PX (PY , dY , bY ) → (PY ) PY := PEAF bX Glg. (8.5) Glg. (8.4) PX (PY , dY , bY ) → (PY , JY ) PY := PEAF , JY := 0 bX Glg. (8.5) Glg. (8.4) Analysemethode Auf Basis der Kopplung von Ereignisstr¨ men lassen sich nun Echtzeitanalyseans¨ tze o a miteinander kombinieren. Dies wird anhand eines Beispiels aus [380] veranschau- licht. Beispiel 8.2.6. Gegeben ist das System in Abb. 8.32. Das System besteht aus zwei Komponenten CPU1 und CPU2, welche die Analysedom¨ nen festlegen. Jeder der a beiden Prozessoren f¨ hrt je zwei Prozesse aus, wobei die Aktivierungen der Prozesse u p1 und p2 durch die Umgebung erfolgen. Der Prozess p1 wird dabei mit einer Pe- riode Pp1 ,in := 40ms aktiviert. Prozess p2 wird mit einer Periode von Pp2 ,in := 20ms aktiviert, wobei die Aktivierung einem Jitter J p2 ,in := 5ms unterliegt. Die Prozes- se auf CPU1 werden mittels einer ratenmonotonen Ablaufplanung eingeplant. CPU2 verwendet ein Round-Robin-Ablaufplanungsverfahren, mit den Slotbreiten S(p3 ) := 5ms und S(p4 ) := 3ms. Die Ausf¨ hrungszeiten (BCET und WCET) der Prozesse sind u gegeben zu: δ (p1 ) := [15ms, 17ms], δ (p2 ) := [8ms, 11ms], δ (p3 ) := [10ms, 11ms] und δ (p4 ) := [3ms, 5ms]. Im Folgenden soll die Ende-zu-Ende-Latenz von der Ak- tivierung des Prozesses p1 bis zur Beendigung des Prozesses p3 bzw. von der Ak- tivierung des Prozesses p2 bis zur Beendigung des Prozesses p4 bestimmt werden. Die Echtzeitanalysemethoden f¨ r CPU1 und CPU2 setzen voraus, dass CPU1 le- u diglich rein periodische Eingabeereignisstr¨ me erh¨ lt. Als Ausgabe werden periodi- o a sche Ereignisstr¨ me mit Jitter erzeugt. CPU2 ben¨ tigt sporadische Ereignismodelle o o und erzeugt als Analyseergebnisse ebenfalls sporadische Ereignismodelle. F¨ r die u Analyse m¨ ssen zun¨ chst die Ereignisstr¨ me gekoppelt werden. Hierzu wird am Ein- u a o gang von CPU1 zum Prozess p2 eine Ereignisadaptierungsfunktion (EAF) ben¨ tigt,o da die Umgebung ein periodisches Ereignismodell mit Jitter zur Verf¨ gung stellt, die u Analysemethode jedoch ein rein periodisches Ereignismodell voraussetzt. Zur Kopp- lung der Ereignisstr¨ me zwischen den Prozessen p1 und p3 bzw. p2 und p4 k¨ nnen o o
506 8 Systemveriﬁkation ? ? (P, J) p1 p3 (P) (P) (d) (d) Umgebung CPU1 CPU2 (P, J) (P, J) ? ? (P) (d) (d) p2 p4 Abb. 8.32. Kopplung der Echtzeitanalysemethoden [380] Ereignismodellschnittstellen (EMIFs) nach Tabelle 8.1 zum Einsatz kommen. Das Ergebnis ist in Abb. 8.33 zu sehen. Man sieht, dass die EAFs und EMIFs als weitere Komponenten im Analysemodell auftreten. (P, J) (d) (P, J) p1 p3 (P) (P) (d) (d) Umgebung CPU1 EMIF CPU2 EAF (P, J) (P, J) (P, J) (P) (P) (d) (d) p2 (P, J) p4 (d) Abb. 8.33. Kopplung der Ereignisstr¨ me [380] o F¨ r die EAF ergibt sich nach Tabelle 8.2, dass ein Puffer der Gr¨ ße nEAF = 1 u o verwendet und mit der Periode Pp2 ,in betrieben werden kann. Nun kann die CPU1 analysiert werden. Durch die Antwortzeitanalyse (siehe Gleichung (7.21) auf Sei- te 446) ergibt sich, dass die Antwortzeiten τF (p1 ) und τF (p2 ) der Prozesse p1 bzw. p2 wie folgt gegeben sind: τF (p1 ) = [31ms, 39ms] τF (p2 ) = [8ms, 11ms] Diese Zeiten lassen sich wie folgt erkl¨ ren. Aufgrund der geringeren Periode be- a sitzt Prozess p2 in der ratenmonotonen Ablaufplanung die h¨ here Priorit¨ t. F¨ r die o a u Zeitanalyse wird der Fall betrachtet, dass beide Prozesse die selbe Phase besitzen, also gleichzeitig aktiviert werden. Aufgrund der h¨ heren Priorit¨ t wird p2 zuerst o a ausgef¨ hrt. Die Antwortzeit ergibt sich gem¨ ß der Ausf¨ hrungszeit des Prozesses. u a u Nach Beendigung der Ausf¨ hrung von p2 kann Prozess p1 gestartet werden. Die- u ser wird allerdings durch die n¨ chste Aktivierung von p2 unterbrochen. Aus diesen a Antwortzeiten lassen sich die Ausgabeereignisstr¨ me ableiten: o
8.2 Zeitanalyse auf Systemebene 507 Pp1 ,out = 40ms + − J p1 ,out = τF (p1 ) − τF (p1 ) = 8ms Pp2 ,out = 20ms + − J p2 ,out = τF (p2 ) − τF (p2 ) = 3ms + − Dabei bezeichnen τF und τF die obere bzw. untere Schranke einer Antwortzeit. Die- se Ausgabeereignisstr¨ me m¨ ssen nun an die erwarteten Eingabeereignisstr¨ me von o u o CPU2 angepasst werden. Da in diesem Fall keine Adaptierung der Ereignisstr¨ meo erfolgen muss, k¨ nnen die Umwandlungen aus Tabelle 8.1 direkt verwendet werden. o Die Eingabeereignisstr¨ me ergeben sich dann zu: o d p3 ,in = Pp1 ,out − Jp1 ,out = 32ms d p4 ,in = Pp2 ,out − Jp2 ,out = 17ms Die Echtzeitanalyse auf CPU2 f¨ hrt zu folgenden Antwortzeiten [380] (siehe auch u Gleichung (7.22) auf Seite 447): τF (p3 ) = [13ms, 20ms] τF (p4 ) = [3ms, 15ms] Der jeweils beste Fall ergibt sich, wenn der betreffende Prozess zuerst geplant wird und dieser die BCET zur Ausf¨ hrung ben¨ tigt. Der schlechteste Fall ergibt sich, u o wenn jeweils der andere Prozess zuerst geplant wird und beide Prozesse die WCET zur Ausf¨ hrung ben¨ tigen. u o Abschließend k¨ nnen nun die gesuchten Ende-zu-Ende-Latenzen Λ bestimmt o werden, indem entsprechend der Ereignisstromkopplung die Ergebnisse zusammen- gefasst werden. Es ergibt sich somit: Λ (p1 → p3 ) = τF (p1 ) + τF (p3 ) = [44ms, 59ms] Λ (p2 → p4 ) = τF (p2 ) + τF (p4 ) = [11ms, 26ms] Die kompositionale Zeitanalyse l¨ sst sich somit durch folgende Schritte beschrei- a ben: 1. W¨ hle eine Komponente als Analysedom¨ ne, f¨ r die alle Eingabeereignisstr¨ me a a u o bekannt sind. 2. W¨ hle eine Echtzeitanalysemethode f¨ r diese Analysedom¨ ne. a u a 3. Falls notwendig, passe Eingabeereignisstr¨ me mittels EMIFs bzw. EAFs an. o 4. Bestimme die Antwortzeiten der Prozesse in der Analysedom¨ ne sowie die Aus- a gabeereignisstr¨ me. o 5. Wiederhole Schritte 1 bis 5 bis alle Prozesse analysiert sind. Behandlung zyklischer Abh¨ ngigkeiten a Bisher wurde lediglich die Analyse von Prozessketten beschrieben, wobei die Ana- lyse keine zyklischen Abh¨ ngigkeiten enthielt. Im Allgemeinen kann die Analyse a allerdings zyklische Abh¨ ngigkeiten enthalten, wie das folgende Beispiel aus [380] a zeigt.
508 8 Systemveriﬁkation Beispiel 8.2.7. Abbildung 8.34 zeigt wiederum ein System mit zwei Prozessoren mit je zwei Prozessen. Beide Prozessoren verwenden eine pr¨ emptive priorit¨ tsbasierte a a Ablaufplanung. Auf CPU1 hat Prozess p1 die h¨ here Priorit¨ t, auf CPU2 hat Prozess o a p4 die h¨ here Priorit¨ t. o a p1 p3 (P) Umgebung Umgebung (P) CPU1 CPU2 p2 p4 Abb. 8.34. Zyklische Abh¨ ngigkeiten in der Zeitanalyse [380] a Die zyklische Abh¨ ngigkeit ergibt sich folgendermaßen: Prozess p2 aktiviert a Prozess p4 , der wiederum Prozess p3 in der Ausf¨ hrung unterbrechen kann. Die u Ausf¨ hrung von Prozess p3 aktiviert den Prozess p1 , der seinerseits Prozess p2 un- u terbrechen kann. Man beachte bei diesem Beispiel, dass die Anwendung selbst keine zyklischen Abh¨ ngigkeiten enth¨ lt. Diese ergeben sich erst durch die Ressourcenwiederverwen- a a dung, die in der Zeitanalyse ber¨ cksichtigt werden muss. u Die Zeitanalyse von Systemen mit zyklischen Abh¨ ngigkeiten erfolgt als Fix- a ¨ punktberechnung, indem eine Iteration uber die Berechnung von Ereignisstr¨ meno ¨ solange durchgef¨ hrt wird, bis sich kein Ereignisstrom im System mehr andert. u 8.2.3 Modulare Zeitanalyse mit RTC Im Folgenden wird eine weitere formale Methode, die als modulare Zeitanalyse be- zeichnet wird, vorgestellt. Diese basiert auf dem sog. Echtzeitkalk¨ l (engl. Real Time u Calculus, RTC), einer Erweiterung des Netzwerkkalk¨ ls. Zun¨ chst wird die modula- u a re Zeitanalyse f¨ r Netzwerkprozessoren vorgestellt. Anschließend wird die Anwen- u dung der modularen Zeitanalyse f¨ r zyklische markierte Graphen pr¨ sentiert. u a ¨ Das Echtzeitkalkul Das Netzwerkkalk¨ l ist eine formale Methode, um Zeiteigenschaften in Netzwerken u zu analysieren. Dabei werden die Beschr¨ nkungen, die beim Transport der Pake- a te durch beschr¨ nkte Kapazit¨ ten der Verbindungen und andere Kommunikationss- a a tr¨ me auftreten, ber¨ cksichtigt. Die Analyse basiert dabei auf Faltungsopertation in o u Max-Plus-Algebra. Das Echtzeitkalk¨ l erweitert das Netzwerkkalk¨ l im Wesentli- u u chen um Aspekte der dynamischen Ablaufplanung in Echtzeitsystemen. Mit dem Echtzeitkalk¨ l lassen sich somit Echtzeitsysteme, die verteilt z. B. als Mehrprozes- u sorsystem implementiert wurden, analysieren.
8.2 Zeitanalyse auf Systemebene 509 Beispiel 8.2.8. Gegeben ist der Netzwerkprozessor in Abb. 8.35, bestehend aus zwei Prozessorkernen (DSP, ARM), zwei Hardware-Beschleunigern (CheckSum, Cipher) und einem Bus. Die Prozessbindung und die Kommunikation zwischen Prozessen ist ebenfalls in Abb. 8.35 gegeben. Die Anwendung beschreibt die Schritte zur Ent- schl¨ sselung eines Datenstroms als Kette aus elf Aktoren. u ARM Cipher a1 a9 a10 a7 a2 a3 a4 Bus a0 a8 a6 a5 CheckSum DSP a0 : Verify IP Header a4 : AH Verify a8 : Calc Check Sum a1 : Process IP Header a5 : ESP Decaps a9 : ARP Look Up a2 : Classify a6 : Route Look Up a10 : Schedule a3 : Decrypt a7 : IP Header Modify Abb. 8.35. Paketverarbeitung in einem Netzwerkprozessor [429] F¨ r die Zeitanalyse muss bekannt sein, wie viele Datenpakete jeder Prozess zu u verarbeiten hat. Dabei wird von der tats¨ chlichen Anzahl abstrahiert und, mit Hilfe a sog. Ankunftskennlinien, die minimale und maximale Anzahl an Aktivierungen eines Prozesses pro Zeitintervall Δ angeben, beschrieben. Deﬁnition 8.2.1 (Ankunftskennlinie). Eine untere bzw. obere Ankunftskennlinie α l und α u bilden ein positives Zeitintervall Δ ∈ T auf die minimale bzw. maximale Anzahl an Aktivierungen eines Prozesses im Zeitintervall Δ ab, d. h. α l,u : T → R≥0 . In Deﬁnition 8.2.1 beschreibt T alle m¨ glichen Zeitpunkte. Im Folgenden wird ange- o nommen, dass T := R≥0 ist. Die Schranken der Aktivierungen werden als kontinu- ierliche Gr¨ ße dargestellt. Der Fall, dass die Aktivierungen nur als diskrete Gr¨ ßen o o auftreten, ist darin enthalten. Die Ankunftskennlinien k¨ nnen beispielsweise aus Simulationstraces gewonnen o werden, indem ein Fenster der Gr¨ ße Δ uber dem Trace verschoben wird, und die mi- o ¨ nimale und maximale Anzahl an Aktivierungen eines Prozesses in diesem Zeitfenster auf dem Trace bestimmt wird. Manchmal lassen sich die Ankunftskennlinien auch
510 8 Systemveriﬁkation aus der Speziﬁkation konstruieren. Treten beispielsweise Aktivierungen mit einem bekannten Muster auf, so kann dieses Muster in die minimale und maximale An- kunftskennlinie transformiert werden. Ein Beispiel f¨ r solche Speziﬁkationen sind u die im vorherigen Abschnitt eingef¨ hrten Ereignisstr¨ me. Dabei wird jedes Ereignis u o als Aktivierung eines Prozesses interpretiert. F¨ r die in Abb. 8.27 auf Seite 500 ein- u gef¨ hrten Ereignisstr¨ me sind die Ankunftskennlinien in Abb. 8.36 dargestellt. Die u o unteren Ankunftskennlinien sind gestrichelt gezeichnet. a) periodisch b) periodisch mit Jitter c) periodisch mit Bursts αl, αu αl, αu αl, αu 4 4 4 3 3 3 2 2 2 1 1 1 P 2P Δ P 2P Δ d P 2P Δ P−J P+J 2P − J 2P + J Abb. 8.36. Ankunftskennlinien f¨ r die Ereignisstr¨ me aus Abb. 8.27 [435] u o Neben der Modellierung der Prozesse m¨ ssen ebenfalls die Ressourcen in der u Architektur modelliert werden. Hierzu z¨ hlen die Prozessoren und die Hardware- a Beschleuniger, aber auch die Busse. Die M¨ glichkeiten Berechnungen oder Kommu- o nikationen durchzuf¨ hren, werden im Echtzeitkalk¨ l mittels sog. Servicekennlinien u u beschrieben. Deﬁnition 8.2.2 (Servicekennlinie). Eine untere bzw. obere Servicekennlinie β l und β u bilden ein positives Zeitintervall Δ ∈ T auf die minimal bzw. maximal verf¨ gbare u Rechenzeit einer Ressourcen in jedem Zeitintervall der Gr¨ ße Δ ab. Es gilt β l (0) = o β u (0) := 0 und ∀τ > 0, Δ > 0 : β l (Δ ) ≤ c(τ + Δ ) − c(τ ) ≤ β u (Δ ) , wobei c(τ ) die bis zum Zeitpunkt τ kumulative verf¨ gbare Rechenzeit darstellt. u Dies bedeutet, dass jede Servicefunktion, die innerhalb der unteren β l und obe- ren Servicekennlinie β u liegt, durch β l und β u charakterisiert werden kann. Ab- bildung 8.37 zeigt die Servicekennlinien einer TDMA-Ablaufplanung. Die untere Servicekennlinie ist dabei gestrichelt gezeichnet. Durch Ausf¨ hrung eines Prozesses wird die Servicekennlinie ver¨ ndert, da nach u a Ausf¨ hrung des Prozesses weniger Rechenkapazit¨ t zur Verf¨ gung steht als vorher. u a u ¨ Um die Anderung allerdings bestimmen zu k¨ nnen, m¨ ssen die Ankunftskennlinien o u modiﬁziert werden. Dies ist notwendig, da die Ankunftskennlinien α l und α u die
8.2 Zeitanalyse auf Systemebene 511 β l, β u 3·b·d 2·b·d d Bandbreite b b·d τ d P−d 2·P 3·P Δ P Abb. 8.37. Servicekennlinie einer TDMA-Ablaufplanung [435] minimalen und maximalen Aktivierungen eines Prozesses angeben. Diese m¨ ssen u zun¨ chst in eine Rechenlast umgerechnet werden. a Sei w die Rechenlast pro Aktivierung eines Prozesses, so k¨ nnen die Schran- o ken an die Rechenlast, verursacht durch diesen Prozess, berechnet werden. Diese Schranken werden wiederum als Ankunftskennlinien beschrieben. Sei [α l , α u ] ein Intervall, das die Anzahl der Aktivierungen eines Prozesses beschr¨ nkt. Dann kann a die Rechenlast durch diesen Prozess mit Ausf¨ hrungszeit w wie folgt beschr¨ nkt u a werden: [α l , α u ] := [w · α l , w · α u ] (8.6) Mit den Ankunftskennlinien α l und α u f¨ r einen Prozess sowie den Service- u kennlinien β l und β u einer Ressource lassen sich die Schranke β l und β u f¨ r die u verbleibende Rechenzeit der Ressource bestimmen, wenn der Prozess auf der Res- source ausgef¨ hrt wird [430]: u β l (Δ ) := sup {β l (λ ) − α u (Δ )} (8.7) 0≤λ ≤Δ β u (Δ ) := sup {β u (λ ) − α l (Δ )} (8.8) 0≤λ ≤Δ Das Supremum (auch obere Schranke) bezeichnet das kleinste Element, das gr¨ ßero oder gr¨ ßer gleich allen Elementen der gegeben Menge ist. o Weiterhin k¨ nnen die Ankunftskennlinie α l und α u f¨ r die Prozessausf¨ hrung o u u auf einer Ressource mit Servicekennlinien β l und β u bei Aktivierung des Prozesses mit Ankunftskennlinien α l und α u bestimmt werden [430]: α l (Δ ) := inf {α l (λ ) + β l (Δ − λ )} (8.9) 0≤λ ≤Δ α u (Δ ) := inf {sup{α u (λ + ν ) − β l (ν )} + β u (Δ − λ ), β u (Δ )} (8.10) 0≤λ ≤Δ ν ≥0 Das Inﬁmum (auch untere Grenze) ist das gr¨ ßte Element, dass kleiner oder kleiner o gleich allen Elementen der gegeben Menge ist.
512 8 Systemveriﬁkation Um aus den Ankunftskennlinien f¨ r die Prozessausf¨ hrung wieder in Ankunfts- u u kennlinien f¨ r die Aktivierung eines datenabh¨ ngigen Prozesses umzuwandeln, kann u a f¨ r jedes Intervall [α l , α u ] ein Intervall der folgenden Form berechnet werden: u αl αu [α l , α u ] := , (8.11) w w In Abb. 8.38 ist die Transformation der Ankunfts- und Servicekennlinien gra- phisch als Blockdiagramm dargestellt. Durch Verschalten dieser Bl¨ cke mit weite- o ren Bl¨ cken k¨ nnen, z. B. durch die Ankunftskennlinien, weitere Prozesse aktiviert o o bzw. die verbleibende Rechenleistung einer Ressource f¨ r andere Prozesse verwen- u det werden. Durch die Verschaltung entsteht ein sog. Zeitbewertungsnetzwerk, wel- ches zur Bestimmung der erreichbaren Latenzen verwendet werden kann. [β l , β u ] [α l , α u ] Glg. (8.6) Glgn. (8.7)–(8.10) Glg. (8.11) [α l , α u ] [β l , β u ] Abb. 8.38. Transformation der Ankunfts- und Servicekennlinien [429] Beispiel 8.2.9. Zur Analyse des Zeitverhaltens zweier Prozesse auf einem einzelnen Prozessor, die mittels statischer Priorit¨ ten pr¨ emptiv und dynamisch geplant wer- a a den, kann das in Abb. 8.39 dargestellte Zeitbewertungsnetzwerk verwendet werden. Die verf¨ gbare Rechenzeit des Prozessors im Idle-Zustand ist durch die Servicekenn- u linien β l und β u beschr¨ nkt. Die Ankunftskennlinien α l und α u sowie α l und α u a 0 0 1 1 beschreiben die Aktivierungen der beiden Prozesse. Prozess 0 hat die h¨ here Prio- o rit¨ t. Man sieht, dass die verbleibende Rechenzeit, beschr¨ nkt durch β l und β u , a a dem Prozess 1 zur Verf¨ gung gestellt wird. u Durch die Verschaltung der einzelnen Bl¨ cke kann das Zeitbewertungsnetzwerk o St¨ ck f¨ r St¨ ck aus Teilsystemen (Modulen) zusammengesetzt werden, weshalb die- u u u se Analysemethode als modulare Zeitanalyse bezeichnet wird. Bestimmung der maximalen Latenzen und des maximalen Backlogs Mit einem Zeitbewertungsnetzwerk ist es nun m¨ glich, die Latenz, aber auch den o Backlog in Netzwerkprozessoren zu beschr¨ nken. Bei der Latenz handelt es sich um a die maximale Ende-Zu-Ende-Latenz eines Datenpakets, dass durch den Netzwerk- prozessor verarbeitet wird. Der Backlog gibt den maximalen Speicherbedarf eines
8.2 Zeitanalyse auf Systemebene 513 [β l , β u ] [α0 l , α0 u ] Glg. (8.6) Glgn. (8.7)–(8.10) Glg. (8.11) [ α0 l , α0 u ] [β l , β u ] [α1 l , α1 u ] Glg. (8.6) Glgn. (8.7)–(8.10) Glg. (8.11) [α1 l , α1 u ] [β l , β u ] Abb. 8.39. Pr¨ emptive Ablaufplanung mit statischen Priorit¨ ten [429] a a Datenstroms im Netzwerkprozessor an. Mit Ergebnissen des Netzwerkkalk¨ ls las- u sen sich die Latenz Λ und der Backlog Ω wie folgt beschr¨ nken: a Λ := sup {inf{τ ≥ 0 : α u (λ ) ≤ β l (λ + τ )} (8.12) λ ≥0 Ω := sup {α u (λ ) − β l (λ )} (8.13) λ ≥0 Somit ist die maximale Latenz durch den maximalen horizontalen Abstand, und der maximale Backlog durch den maximalen vertikalen Abstand zwischen α u und β l beschr¨ nkt. a Zur Bestimmung der Werte durch Gleichung (8.12) und (8.13) muss zun¨ chst ge- a kl¨ rt werden, welches α u und welches β l zu verwenden ist. F¨ r die Ankunftskenn- a u linie ist der Fall klar: α u ist die obere Ankunftskennlinie f¨ r den ersten Prozess in u der Verarbeitungskette, da diese Aktivierung durch die Umgebung begrenzt ist, d. h. durch die Anzahl der zu verarbeitenden Pakete. Bei der Rechenzeitbeschr¨ nkung a handelt es sich um die kumulierte Rechenzeitbeschr¨ nkung entlang der Kette von a Prozessen, die ein Datenpaket bearbeiten. Seien β0 , β1 , . . . , βm−1 die unteren Ser- l l l vicekennlinien der Ressourcen entlang des Verarbeitungspfads, dann l¨ sst sich die a kumulierte Servicekennlinie β l durch sukzessive Faltung berechnen: l β 0 := β0 l l l β i+1 := inf {β i + βi+1 (Δ − λ )} ∀i ≥ 1 l (8.14) 0≤λ ≤Δ l β l := β m Beispiel 8.2.10. Das Zeitbewertungsnetzwerk f¨ r die Entschl¨ sselung eines Daten- u u stroms auf dem Netzwerkprozessor in Abb. 8.35 auf Seite 509 ist in Abb. 8.40 zu
514 8 Systemveriﬁkation sehen. Die runden Knoten bezeichnen dabei Quellen bzw. Senken von Ankunfts- und Servicekennlinien, d. h. sie modellieren die Umgebung des Systems. So wird beispielsweise die Ankunftsrate von Paketen beschr¨ nkt. Die Rechtecke bezeichnen a die Transformation der Ankunfts- und Servicekennlinien entsprechend Abb. 8.38. Man beachte, dass im Echtzeitkalk¨ l Kommunikation genauso wie Berechnungen u auf Prozessoren behandelt wird. CheckSum Bus ARM Cipher DSP in in in in in in a0 com a1 a2 com a3 a4 com a5 a6 com a7 com a8 com a9 a10 out out out out out out Abb. 8.40. Zeitbewertungsnetzwerk f¨ r den Netzwerkprozessor aus Abb. 8.35 [429] u Modulare Zeitanalyse zyklischer markierter Graphen In Abschnitt 6.5.2 wurde eine formale Methode zur Zeitanalyse von latenzinsen- sitiven Systemen vorgestellt. Das zentrale Ergebnis war, dass sich solche Systeme als markierte Graphen modellieren lassen (siehe Abb. 6.82 auf Seite 356). Da Im- plementierungen mit beschr¨ nktem Speicher auskommen m¨ ssen, wurden FIFO- a u Kan¨ le mit beschr¨ nkter Kapazit¨ t durch zus¨ tzliche r¨ ckw¨ rts gerichtete Kanten a a a a u a
8.2 Zeitanalyse auf Systemebene 515 mit Anfangsmarkierung modelliert. Dadurch wurden Ressourcenbeschr¨ nkungen f¨ r a u die Kan¨ le ber¨ cksichtigt. Ressourcenbeschr¨ nkungen f¨ r die Aktoren wurden durch a u a u Selbstschleifen mit einer einzelnen Anfangsmarke modelliert, wodurch ein Aktor stets erst nach Beendigung einer Berechnung die n¨ chste Berechnung starten kann. a Aktoren sind in diesem Modell dediziert gebunden, d. h. jeder Aktor entspricht ei- ner Hardware-Komponente. In diesem Abschnitt wird beschrieben, wie die modu- lare Zeitanalyse f¨ r Systeme, bei denen mehrere Aktoren auf die selben Hardware- u Komponente gebunden sein k¨ nnen, angewendet werden kann. o Modellierung markierter Graphen Gegeben sei ein markierter Graph G = (A,C, M0 ) mit Aktoren a ∈ A, Kan¨ len a c ∈ C ⊆ A × A und der Anfangsmarkierung M0 : C → R≥0 . Man beachte, dass die Markierung eines Kanals kontinuierlich sein kann. Dies schließt selbstverst¨ ndlich a den Fall ein, dass Marken diskret sein k¨ nnen. Ein Aktor verarbeitet einen Strom aus o Marken, der als Ereignisstrom modelliert wird. Die Anzahl zu verarbeitender Marken, die in einem Kanal (vi , v j ) gespeichert wurden, wird als sog. Ankunftsfunktion ri j (τ ) : T → R≥0 modelliert. Diese weist je- dem Zeitpunkt τ ∈ T die Anzahl an Marken zu, die im Zeitintervall [0, τ ) an dem Kanal (vi , v j ) angekommen sind. Dies entspricht der Anzahl produzierter informati- ver Daten eines Aktors in einem latenzinsensitiven System (siehe Gleichung (6.26)). Die Anfangsmarkierung des Kanals ergibt sich zu ri j (0) := M0 (vi , v j ). F¨ r einen Aktor ai ∈ A lassen sich die Ankunftsfunktionen der Eingangskan¨ le u a zu einem Vektor riin zusammenfassen: riin := (r ji | (v j , vi ) ∈ C). Analog lassen sich die Ankunftsfunktionen der Ausgangskan¨ le in einem Vektor riout zusammenfassen: a riout := (rik | (vi , vk ) ∈ C). Man sagt, f¨ r zwei Vektoren riin und riin von Ankunftsfunk- u ˜ tionen, dass riin ≥ riin ist, falls ∀(a j , ai ) ∈ A, τ ∈ T gilt, dass riin (τ ) ≥ riin (τ ) ist. ˜ j ˜j Das zeitliche Verhalten eines Aktors ai l¨ sst sich als Abbildung der Ankunfts- a funktionen der Eingangskan¨ le riin auf die Ankunftsfunktionen der Ausgangskan¨ le a a riout beschreiben: riout : πi ◦ riin (8.15) πi wird als Transferfunktion des Aktors ai bezeichnet. Da Aktoren in markierten Graphen deterministisches Verhalten besitzen, beschreibt πi eine deterministische Abbildung. Weiterhin besitzen markierte Graphen monotones Verhalten, d. h., falls riin ≥ riin gilt, dass πi ◦ riin ≥ πi ◦ riin . ˜ ˜ Ohne Ressourcenbeschr¨ nkungen bei selbstplanender Ausf¨ hrung der Aktoren a u gilt, dass die Anzahl der produzierten Marken eines Aktors ai auf jedem Ausgangs- kanal gleich dem Minimum der auf seinen Eingangskan¨ len verarbeitbaren Marken a ist (siehe auch Gleichung (6.28) auf Seite 354): ∀(vi , vk ) ∈ C : rik (τ ) := min {rin (τ )} out ji (8.16) (v j ,vi )∈C Bei der selbstplanenden Ausf¨ hrung von Aktoren feuern diese, sobald gen¨ gend u u Marken auf den Eingangskan¨ len verf¨ gbar sind. a u
516 8 Systemveriﬁkation Die Ankunftsfunktionen der Ausgangskan¨ le eines Aktors ai stellen f¨ r andere a u Aktoren oder ai selbst Ankunftsfunktionen f¨ r Eingangskan¨ le dar. Aufgrund der u a FIFO-Semantik der Kan¨ le in markierten Graphen m¨ ssen die Ankunftsfunktionen a u um die Anfangsmarkierung verschoben werden. Dies kann durch die Sprungfunktion ρ ji (τ ) f¨ r einen Kanal (v j , vi ) dargestellt werden: u 0 falls τ ≤ 0 ρ ji (τ ) := M0 (v j , vi ) falls τ > 0 Damit kann der Zusammenhang zwischen der Ankunftsfunktion r out (τ ) auf einem ji Ausgangskanal eines Aktors a j und der Ankunftsfunktion rin (τ ) f¨ r den selben Ka- ji u nal beim lesenden Aktor ai hergestellt werden: rin (τ ) := rout (τ ) + ρ ji (τ ) ji ji (8.17) Gleichungen (8.16) und (8.17) lassen sich zu einem Gleichungssystem zusammen- fassen (siehe auch Gleichung (6.30) auf Seite 354): r := Π ◦ r (8.18) Dabei enth¨ lt r die Ankunftsfunktionen an den Ausgabekan¨ len (v j , vi ) ∈ C, d. h. a a r := (rout | (v j , vi ) ∈ C), und Π enth¨ lt die Abbildungsfunktionen aller Aktoren. ji a Diese Gleichung besitzt einen eindeutigen Fixpunkt, setzt man δ -Kausalit¨ t voraus, a d. h. dass Marken fr¨ hestens einen kurzen Zeitschritt δ > 0, nachdem sie produziert u worden sind, einen folgenden Aktor aktivieren k¨ nnen. Liegen keine Ressourcenbe- o schr¨ nkungen vor, kann der maximale Durchsatz des markierten Graphen auf Ba- a sis von Max-Plus-Algebra bestimmt werden (siehe Abschnitt 6.5.2). Der Fixpunkt charakterisiert den Eigenwert der Matrix Π und damit den Durchsatz. Beschr¨ nktea Kanalkapazit¨ ten k¨ nnen durch R¨ ckkanten modelliert werden. a o u Modellierung von Ressourcenbeschr¨ nkungen a Um zu modellieren, dass die Ausf¨ hrung eines Aktors ai Ressourcenbeschr¨ nkun- u a gen unterliegt, muss die Abbildungsfunktion πi angepasst werden [432]. Hierzu wird angenommen, dass der Aktor ai auf einer Ressource ausgef¨ hrt wird, die durch eine u sog. Servicefunktion c(τ ) beschrieben wird. Dabei beschreibt c(τ ) ∈ R≥0 die An- zahl an Aktorfeuerungen, welche die Ressource in dem Zeitintervall [0, τ ) ausf¨ hren u kann, wobei c(0) := 0 ist. Die Verwendung von Servicefunktionen erlaubt eine Modellierung beliebiger Ressourcenbeschr¨ nkungen und Ablaufplanungsstrategien. Das Kommunikations- a verhalten eines Aktors ai mit einem Aktor k bei selbstplanender Ausf¨ hrung kann u unter Ber¨ cksichtigung von Ressourcenbeschr¨ nkungen mit der folgenden Transfer- u a funktion beschrieben werden: rik (τ ) := inf { min {rin (λ )} + c(τ ) − c(λ )} out ji (8.19) 0≤λ ≤τ (v j ,vi )∈C
8.2 Zeitanalyse auf Systemebene 517 Gleichung (8.19) kann dann wie folgt interpretiert werden [432]: In einem Inter- vall [λ , τ ) k¨ nnen c(τ ) − c(λ ) Aktorfeuerungen ausgef¨ hrt werden, sofern gen¨ gend o u u Marken am Eingang verf¨ gbar sind, d. h. rik (τ ) ≤ rik (λ ) + c(τ ) − c(λ ). Wei- u out out terhin muss zu jedem Zeitpunkt gelten, dass rik (λ ) ≤ min(v j ,vi )∈C {rin (λ )} ist, da out ji ein Aktor h¨ chstens so viele Marken produzieren kann, wie auf einem Eingangs- o kanal verf¨ gbar waren. Ohne Ressourcenbeschr¨ nkung w¨ rde bei selbstplanender u a u Ausf¨ hrung gelten, dass beide Seiten der Ungleichung gleich sind. Zusammen gilt u rik (τ ) ≤ min(v j ,vi )∈C {rin (λ )} + c(τ ) − c(λ ). out ji Nun gibt es einen Zeitpunkt λ ∗ wo zum letzten Mal galt, dass rik (λ ∗ ) = out ∗ ∗ ∗ min(v j ,vi )∈C {r ji (λ )} ist. Dieser Zeitpunkt kann entweder λ = 0, λ = τ oder ein in Zeitpunkt dazwischen sein. Nach diesem Zeitpunkt λ ∗ ist die Ressource perma- nent mit der Ausf¨ hrung des Aktors ai ausgelastet. Es gilt: rik (τ ) = rik (λ ∗ ) + u out out ∗ in (λ ∗ )} + c(τ ) − c(λ ∗ ). Genau dieses λ ∗ wird mit der c(τ ) − c(λ ) = min(v j ,vi )∈C {r ji Inﬁmum-Operation bestimmt, die in der Transferfunktion in Gleichung (8.19) ange- geben ist. Beispiel 8.2.11. Gegeben ist der markierte Graph in Abb. 8.41 mit drei Aktoren. Je- der Aktor ai wird auf einer Ressource mit der Servicefunktion ci (τ ) ausgef¨ hrt. Die u Transferfunktionen f¨ r den markierten Graph ergeben sich unter Verwendung von u Gleichung (8.19) und (8.17) dann zu: r0,1 (τ ) := inf {r1,0 (λ ) + c0 (τ ) − c0 (λ )} out in 0≤λ ≤τ = inf {r1,0 (λ ) + ρ1,0 (λ ) + c0 (τ ) − c0 (λ )} out 0≤λ ≤τ r1,2 (τ ) := inf {min{r0,1 (λ ), r2,1 (λ )} + c1 (τ ) − c1 (λ )} out in in 0≤λ ≤τ = inf {min{r0,1 (λ ), r2,1 (λ ) + ρ2,1 (λ )} + c1 (τ ) − c1 (λ )} out out 0≤λ ≤τ r2,1 (τ ) := inf {r1,2 (λ ) + c2 (τ ) − c2 (λ )} out in 0≤λ ≤τ = inf {r1,2 (λ ) + c2 (τ ) − c2 (λ )} out 0≤λ ≤τ r1,0 (τ ) := inf {min{r0,1 (λ ), r2,1 (λ )} + c1 (τ ) − c1 (λ )} out in in 0≤λ ≤τ = inf {min{r0,1 (λ ), r2,1 (λ ) + ρ2,1 (λ )} + c1 (τ ) − c1 (λ )} out out 0≤λ ≤τ a0 a1 a2 Abb. 8.41. Markierter Graph [432]
518 8 Systemveriﬁkation Die verbleibende Servicefunktion c (τ ) nachdem ein Aktor ai ausgef¨ hrt wurde, u ergibt sich zu: c (τ ) := c(τ ) − min {rin (τ )} ji (8.20) (v j ,vi )∈C Abstraktion der Servicefunktion Um die Zeitanalyse efﬁzient durchf¨ hren zu k¨ nnen, m¨ ssen sowohl die Service- u o u funktionen als auch die Ankunftsfunktionen abstrahiert werden. Zun¨ chst werden a die Servicefunktionen durch untere und obere Schranken begrenzt. Diese Schran- ken werden als Servicekennlinien (siehe Deﬁnition 8.2.2 auf Seite 510) bezeichnet. Dabei wird von dem Zeitbereich in den Zeitintervallbereich gewechselt. Unter Verwendung von Servicekennlinien βil und βiu f¨ r den Aktor ai kann Glei- u chung (8.19) wie folgt angen¨ hert werden: a rik (τ ) ≤ inf { min {rin (λ )} + βiu (τ − λ )} out ji 0≤λ ≤τ (v j ,vi )∈C rik (τ ) out ≥ inf { min {rin (λ )} + βil (τ − λ )} ji 0≤λ ≤τ (v j ,vi )∈C Unter Verwendung des Operators a ⊕ b := min{a, b} und des Operators a(τ ) ⊗ b(τ ) := inf0≤λ ≤τ {a(λ ) − b(τ − λ )} erh¨ lt man: a ⎛ ⎞ ⎛ ⎞ ⎝ rin (τ )⎠ ⊗ βil (τ ) ≤ rik (τ ) ≤ ⎝ ji out rin (τ )⎠ ⊗ βiu (τ ) ji (8.21) (v j ,vi )∈C (v j ,vi )∈C In [432] beweisen Thiele und Stoimenov: Wenn die Servicefunktion c(τ ) durch die Servicekennlinien ersetzt wird, erh¨ lt man untere bzw. obere Schranken f¨ r die a u Ankunftsfunktion. ⎛ ⎞ rik (τ ) ≥ βil (τ ) ⊕ ⎝ out (rout (τ ) ⊗ (ρ ji (τ ) + βil (τ )))⎠ ji (v j ,vi )∈C ⎛ ⎞ rik (τ ) ≤ βiu (τ ) ⊕ ⎝ out (rout (τ ) ⊗ (ρ ji (τ ) + βiu (τ )))⎠ ji (v j ,vi )∈C Unter Verwendung der Matrixmultiplikation C = A ⊗ B mit ci j := k (aik ⊗ bk j ) k¨ nnen diese Ungleichungen kompakt als o rl := β l ⊕ Sl ⊗ rl ru := β u ⊕ Su ⊗ ru mit βil,u + M0 (v j , vi ) falls (v j , vi ) ∈ C sl,u := ij ∞ sonst
8.2 Zeitanalyse auf Systemebene 519 dargestellt werden. Dabei stellt Sl bzw. Su die Systemmatrix, β l bzw. β u den Vektor der unteren bzw. oberen Servicekennlinien und r l bzw. ru den Vektor der unteren bzw. oberen Schranken an die Ankunftsfunktionen dar. F¨ r die Systemmatrizen Sl und Su kann der Abschluss bestimmt werden, der wie u folgt deﬁniert ist: ∞ S∗ := S(k) mit S(k) := S ⊗ S(k−1) k:=0 Damit lassen sich schließlich die unteren und oberen Schranken der Ankunftsfunkti- on bestimmen [432]: rl := (Sl )∗ ⊗ β l (8.22) ru := (Su )∗ ⊗ β u (8.23) Maximale Latenzen in markierten Graphen Um die maximalen Latenzen in einem markiertem Graphen mittels der modularen Zeitanalyse bestimmen zu k¨ nnen, werden zwei durch einen Pfad verbundene Akto- o ren des markierten Graphen ausgew¨ hlt: as sei der Quellaktor und ad sei der Zielak- a tor. Es wird angenommen, dass der Quellaktor as mit der zus¨ tzlichen Ankunftsfunk- a tion gs (τ ) angeregt wird. Es soll dann die maximale Latenz einer Aktivierung des Quellaktors as bis zur Aktivierung des Zielaktors ad bestimmt werden. Die zus¨ tzli- a che Ankunftsfunktion kann dann als Diagonalmatrix Gs angegeben werden. Beispiel 8.2.12. Gegeben ist der markierte Graph mit Eingangsankunftsfunktion am Aktor a0 in Abb. 8.42. Die Matrix, welche die zus¨ tzliche Ankunftsfunktion model- a liert, l¨ sst sich wie folgt beschreiben: a ⎛ ⎞ g0 0 0 Gs := ⎝ 0 ∞ 0 ⎠ 0 0 ∞ Man sieht, dass auf der Diagonalen zus¨ tzliche Eingangsfunktionen f¨ r Aktoren ein- a u getragen werden k¨ nnen. Besitzt ein Aktor keinen Eingang, so ist der entsprechende o Eintrag ∞. Die Nebendiagonalelemente erhalten den Wert null. g0 a0 a2 a1 Abb. 8.42. Markierter Graph mit Eingangsankunftsfunktion
520 8 Systemveriﬁkation Mit der Matrix Gs lassen sich die Gleichungen (8.22) und (8.23) um den Eingang an Aktor as erweitern: rl := (Sl )∗ ⊗ Gs ⊗ β l (8.24) ru := (Su )∗ ⊗ Gs ⊗ β u (8.25) Betrachtet man nun lediglich den Zielaktor ad , so ergibt sich f¨ r die untere An- u kunftsfunktion nach Umformung folgende Gleichung: rd := βsd ⊗ Gs ⊕ hs d l mit l l (8.26) βsd l := (Sl )∗ ⊗ βsl ds und hl sd := {(Sl )∗ j ⊗ β jl } d i= j Darin beschreibt βsd die untere kumulierte Servicekennlinie und hl beschreibt die l sd Transferfunktion des markierten Graphen entlang des Pfades von as nach ad , wenn die Ankunftsfunktion keine Marken enth¨ lt. Es handelt sich somit um einen konstan- a ten Offset. F¨ r die Zeitanalyse wird schließlich noch die Eingangsankunftsfunktion gs durch u Ankunftskennlinien γs und γs begrenzt. Die maximale Latenz von as zu ad l¨ sst sich l u a dann nach Gleichung (8.12) auf Seite 513 berechnen zu: Λsd := max{inf{λ ≥ 0 : βsd (τ − λ ) ≥ γs (τ )∀τ ≥ 0}, l u inf{λ ≥ 0 : hl (τ − λ ) ≥ γs (τ )∀τ ≥ 0}} sd u 8.3 Literaturhinweise Die CTL-Modellpr¨ fung f¨ r SysteMoC-Modelle ist in [191] beschrieben. Sie beruht u u auf der symbolischen Repr¨ sentation des Zustandsraums eines SysteMoC-Modells a auf Basis von IDDs und IMDs [193, 192]. Dabei handelt es sich um eine Verfei- nerung der symbolischen Repr¨ sentation des Zustandsraums f¨ r FunState-Modelle a u [415, 418, 414]. Der Zustandsraum eines FunState-Modells wird dabei als regul¨ rer a Zustandsautomat [434] modelliert. Die dort pr¨ sentierten Verfahren eignen sich auch a zur Modellpr¨ fung von Petri-Netzen [416, 442]. u Die Modellpr¨ fung von SystemC-Modellen ist in [271] vorgestellt. Diese basiert u ¨ auf Vorarbeiten zur Veriﬁkation von SpecC-Modellen [244] und der Aquivalenz- pr¨ fung von Verilog- und C-Programmen [270]. Die Veriﬁkationsmethode verwen- u det dabei attributierte temporale Strukturen f¨ r jeden SystemC-Prozess [89]. Das u ¨ Gesamtmodell erh¨ lt man uber eine parallel Komposition der temporalen Struktu- a ren, wie sie bereits in [14] vorgeschlagen wurde. Die verwendete Abstraktion ist identisch mit der existentiellen Abstraktion“ f¨ r temporale Strukturen [101]. u ” Die in [271] beschriebene formale Modellpr¨ fung kann auch zur Veriﬁkation u von Transaktionsebenenmodellen (TLMs) eingesetzt werden. In [345, 347] ist ein
8.3 Literaturhinweise 521 solcher Ansatz beschrieben. Eine Erweiterung der Transaktionen um die ACID- Eigenschaften (engl. Atomicity, Consistency, Isolation, and Durability) erlaubt es, das Modell des SystemC-Simulators vollst¨ ndig zu eliminieren [346]. Die ACID- a Eigenschaften sind aus Datenbanksystemen bekannt und beschreiben in TLMs fol- gende Eigenschaften: • Atomarit¨ t: Entweder wird eine Transaktion exklusiv, d. h. ohne Verschr¨ nkung a a mit anderen Transaktionen, und vollst¨ ndig auf einem Target ausgef¨ hrt oder gar a u nicht. Man beachte, dass nichtblockierende Transaktionen als mehrere atomare Transaktionen modelliert werden k¨ nnen. o • Konsistenz: Das Target, welches die Transaktion ausf¨ hrt, ist zu Beginn und am u Ende der Ausf¨ hrung in einem g¨ ltigen Zustand. u u • Isolierung: Es sind keine Zwischenzust¨ nde der Berechnung einer Transaktion a außerhalb des Targets sichtbar. • Nachhaltigkeit: Nachdem die erfolgreiche Abarbeitung einer Transaktion best¨ - a tigt wurde, wird diese nicht mehr r¨ ckg¨ ngig gemacht. u a Weitere Ans¨ tze zur formalen Modellpr¨ fung von TLMs ﬁnden sich beispielsweise a u [210] und [337]. Der in Abschnitt 8.1.4 beschriebene zusicherungsbasierte Veriﬁkationsansatz f¨ r u TLMs basiert auf der Verschaltung elementarer Monitore und ist ausf¨ hrlich in u [361] beschrieben. Ein alternativer Ansatz, der spezielle SystemC-Kan¨ le ben¨ tigt, a o ist in [126, 278] beschrieben und verwendet FoCs [167] zur Generierung von C++- ¨ Monitoren. In [344] ist ein simulativer Ansatz zur Uberpr¨ fung von SystemVerilog- u Zusicherungen (SVA) vorgestellt. Mittels Aspekt-orientierter Programmierung wird die Aufzeichnung von zeitbehafteten und nicht zeitbehafteten Transaktionen in die SystemC-TLM-Beschreibung eingeﬂochten. In einem ersten Simulationslauf wer- den somit Verl¨ ufe der Transaktionen aufgezeichnet und anschließend in einer RTL- a u ¨ Simulation bez¨ glich der Zusicherungen uberpr¨ ft. Ein weiterer Ansatz basierend u auf SVA wurde von der Firma Inﬁneon entwickelt [143, 144]. Dieser Ansatz erwei- tert allerdings SVA dahingehend, dass f¨ r TLM-Zusicherungen eine neue Zusicher- u ungssprache ben¨ tigt wird. o Eine Vielzahl an Ans¨ tzen existieren zur Zeitanalyse auf Systemebene, wobei a diese Entwurfsentscheidungen wie Prozessbindung und Transaktionsrouting ber¨ ck-u sichtigen. Diese Ans¨ tze lassen sich in simulative und formale Methoden klassiﬁzie- a ren, wobei simulative Methoden das Problem haben, dass sie unvollst¨ ndig sind. a In der Zeitanalyse bedeutet dies, dass die tats¨ chlichen besten und schlechtesten a F¨ lle im Zeitverhalten einer Implementierung nicht in angemessener Zeit identiﬁ- a ziert werden k¨ nnen. Andererseits sind simulative Methoden breit einsetzbar. Vie- o le simulative Methoden zur Zeitbewertung basieren auf Transaktionsebenenmodel- len [133], wobei Transaktionsebenenmodelle die M¨ glichkeit bieten, die Zeitbe- o wertung durch geeignete Wahl und Kombination von Abstraktionsebenen zu be- schleunigen [387, 391]. Eine quantitative Bewertung der Analysegenauigkeit und -geschwindigkeit f¨ r Transaktionsebenenmodelle des AMBA-Busses ﬁndet sich in u [386].
522 8 Systemveriﬁkation Der in diesem Buch vorgestellte Ansatz zur kombinierten Verhaltens- und Zeit- simulation mittels virtueller Komponenten ist in der VPC-Bibliothek implementiert und ausf¨ hrlich in [419, 215, 420] beschrieben. Ein vergleichbarer Ansatz wurde u in [256] vorgestellt. Um die Laufzeit der simulativen Zeitbewertung zu verringern, bietet es sich an, Daten, die w¨ hrend der Simulation aufgezeichnet werden, in einer a sp¨ teren Analyse wiederzuverwenden. Ein solches Verfahren ist unter dem Namen a Trace-Driven-Simulation bekannt geworden [279, 363]. Eine formale Analyse bei der ebenfalls die Kommunikation im Mittelpunkt steht, ist in [402] beschrieben. Dabei wird ein sog. Kommunikations-Abh¨ ngigkeitsgraph a (engl. communication dependency graph) aus einer gegebenen Implementierung ex- trahiert, um den Einﬂuss der Abbildung auf die Architektur zu analysieren. Dort wer- den kooperative und nicht pr¨ emptive Software-Prozesse als Modell vorausgesetzt a [455]. In [454] wird eine Erweiterung f¨ r zeitschlitzbasierte Ablaufplanung vorge- u stellt. Schließlich ist in [219] eine formale Modellierung von SystemC-Modellen mit zeitbehafteten Automaten beschrieben. Bei den formalen Methoden zur Zeitanalyse k¨ nnen grob holistische und modu- o lare Ans¨ tze unterschieden werden. Holistische Ans¨ tze sind eine direkte Weiterent- a a wicklung der Planbarkeitsanalysen f¨ r Einprozessorsysteme hin zu Mehrprozessor- u systemen. In einer grundlegenden Arbeit kombinierten Tindell und Clark pr¨ emptive a Ablaufplanung auf Basis statischer Priorit¨ ten mit TDMA-Ablaufplanung [441]. Ei- a ne Genauigkeitsverbesserung konnte in [470] erzielt werden. Weitere Busse, wie der CAN- [440] und der FlexRay-Bus [365], wurden in holistischen Verfahren betrach- tet. Bei den modularen Methoden zur formalen Zeitanalyse ist die symbolische Zeitanalyse ein wichtiger Vertreter. Die symbolische Zeitanalyse ist ausf¨ hrlich u in [378, 380, 379, 377] beschrieben. Wichtige Erweiterungen umfassen die Un- terst¨ tzung verschiedener Prozessaktivierungen auf Basis mehrerer Ereignisstr¨ me u o [247, 217] und die Analyse von Datenﬂussmodellen [388]. Die symbolische Zeit- analyse wurde an der Technischen Universit¨ t Braunschweig entwickelt und wird a mittlerweile als Werkzeug SymTA/S [423] von der Firma Symtavision vermarktet und weiterentwickelt. Die modulare Zeitanalyse basiert auf den Netzwerkkalk¨ l, der in [293] beschrie- u ben ist und auf [121] zur¨ ck geht. Hieraus wurde an der ETH Z¨ rich das Echtzeit- u u kalk¨ l entwickelt [431, 430]. Seitdem wurde das Echtzeitkalk¨ l mit anderen Zeit- u u analysemethoden gekoppelt, u. a. simulativen Methoden [277] und zeitbehafteten Automaten [285].
A Notation In diesem Kapitel werden die in diesem Buch verwendeten mathematischen Nota- tionen eingef¨ hrt. Dies erfolgt in Anlehnung an Deﬁnitionen in [426]. u A.1 Mengen Mengen werden mit Großbuchstaben, deren Elemente mit Kleinbuchstaben bezeich- net. {x | P(x)} bezeichne die Menge von Elementen, welche die Bedingung P(x) erf¨ llen. Das Symbol ∈ bezeichne die Mitgliedschaft eines Elementes in einer u Menge. Die Menge von Elementen, deren Elemente genau die Objekte der Liste x1 , x2 , . . . , xm sind, wird mit {x1 , x2 , . . . , xm } bezeichnet. Die leere Menge werde mit ∅ (oder { }) bezeichnet. Zwei Mengen heißen disjunkt, wenn sie kein Element ge- meinsam haben. Die Anzahl der Elemente einer Menge S heißt M¨ chtigkeit von S a und werde mit |S| bezeichnet. Seien A und B Mengen. Man sagt A ist Teilmenge von B, bezeichnet mit A ⊆ B, genau dann, wenn jedes Element von A auch Element von B ist. Wenn A ⊆ B und A = B, dann heißt A echte Teilmenge von B (Schreibweise A ⊂ B). Das relative Komplement von B in A, bezeichnet mit A \ B, ist die Menge {x | x ∈ A ∧ x ∈ B}. Sei A eine Teilmenge einer Menge S. Dann ist das Komplement von A in S die Menge {x | x ∈ S \ A}. Schließlich werde die Vereinigungsmenge mit ∪ und die Schnittmenge mit ∩ bezeichnet. ¨ Die Uberdeckung einer Menge S ist eine Menge von Teilmengen von S mit der Eigenschaft, dass ihre Vereinigung gleich S ist. Eine Partition einer Menge S ist eine ¨ Uberdeckung von S durch disjunkte Teilmengen, sog. Partitionsbl¨ cke. Die Men- o ge aller Teilmengen einer Menge S wird als Potenzmenge 2S bezeichnet. Die leere Menge ∅ ist Element der Potenzmenge jeder beliebigen Menge S, d. h. ∅ ∈ 2S . Die Menge der reellen Zahlen wird mit R, die Menge der rationalen Zahlen mit Q, die Menge der ganzen Zahlen mit Z und die Menge der nat¨ rlichen Zahlen mit u N bezeichnet. Es sei S entweder Z, Q oder R. S+ bezeichne die positive Teilmenge, + S0 oder S≥0 die nichtnegative Teilmenge (insbesondere S+ ∪ {0}) und Sn das n- fache kartesische Produkt von S. Das kartesische Produkt zweier Mengen A und B, bezeichnet mit A × B, ist die Menge von Paaren (a, b), wobei a ∈ A und b ∈ B gilt. C. Haubelt, J. Teich, Digitale Hardware/Software-Systeme, eXamen.press, DOI 10.1007/978-3-642-05356-6, c Springer-Verlag Berlin Heidelberg 2010