Digitale Hardware/ Software-Systeme- Part 16

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

Thêm vào BST

Báo xấu

73
lượt xem 4
download

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

Digitale Hardware/ Software-Systeme- P16: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- Part 16

444 7 Software-Veriﬁkation ∗ ∗ ∗ ∗ ∗ a) τd (v1 ) τd (v1 ) τd (v1 ) τd (v1 ) τd (v1 ) n=0 n=1 n=2 n=3 n=4 CPU v1 v2 v1 v2 v1 v2 v1 v2 v1 v2 n=0 n=1 ∗ ∗ τd (v2 ) τd (v2 ) 0 1 2 3 4 5 6 7 8 9 10 11 τ ∗ ∗ b) τd (v1 ) τd (v1 ) n=0 n=1 CPU v1 v2 v1 v2 v1 v2 n=0 ∗ τd (v2 ) 0 1 2 3 4 5 6 7 8 9 10 11 τ Abb. 7.32. Iterative, dynamische Ablaufpl¨ ne: a) mit der EDF-Strategie und b) mit dem RMS- a Algorithmus Ratenmonotone Ablaufplanung Unter dem Begriff ratenmonotone Ablaufplanung (engl. rate-monotonic scheduling, RMSs) haben Liu und Layland ein pr¨ emptives Ablaufplanungsverfahren beschrie- a ben, das den Prozessen statische Priorit¨ ten nach folgendem Prinzip zuweist: vi habe a gr¨ ßere Priorit¨ t als v j , falls P(vi ) < P(v j ). Also w¨ hlt man die Priorit¨ t statisch bei- o a a a spielsweise proportional zur gegebenen Rate eines Prozesses (Kehrwert der Periode). Prozesse mit kleinerer Periode werden also h¨ her priorisiert als Prozesse mit gr¨ ße- o o rer Periode. Dies gilt also unabh¨ ngig von den Ausf¨ hrungszeiten der Prozesse. Bei a u Ankunft eines Prozesses h¨ herer Priorit¨ t wird der laufende Prozess unterbrochen. o a Beispiel 7.4.5. Abbildung 7.32b) zeigt einen mit der RMS-Strategie gewonnenen Ablaufplan f¨ r das in Beispiel 7.4.4 vorgestellte Problem. u Liu und Layland zeigten dann, dass der RMS-Algorithmus unter allen Algorith- ∗ men mit statischen Priorit¨ ten (f¨ r den von ihnen angenommen Fall τd (vi ) = P(vi )) a u immer einen g¨ ltigen Ablaufplan bestimmt, falls ein solcher existiert. u Beispiel 7.4.6. Aus diesem Ergebnis l¨ sst sich schließen, dass es keinen Algorithmus a mit festen Priorit¨ ten gibt, der f¨ r das Problem aus Beispiel 7.4.4 alle Deadlines a u erf¨ llt, da der RMS-Algorithmus keinen solchen Ablaufplan bestimmt hat. u Nun l¨ sst sich allerdings ein einfaches, hinreichendes Kriterium angeben, wann a der RMS-Algorithmus immer einen Ablaufplan ﬁndet, der alle Deadlines erf¨ llt: u
7.4 Zeitanalyse 445 Theorem 7.4.3 (Liu und Layland). Gegeben sei ein Ablaufplanungsproblem nach ∗ Deﬁnition 7.4.8 mit der Eigenschaft ∀vi ∈ V : τd (vi ) = P(vi ). Die Menge von Prozes- sen kann unter Erf¨ llung aller Deadlines mit dem RMS-Algorithmus geplant werden, u falls |V | δi ∑ P(vi ) ≤ |V | · (21/|V | − 1) (7.19) i:=1 gilt. F¨ r |V | = 1 erh¨ lt man als rechte Seite von Ungleichung (7.19) den Wert 1. Damit u a kann das RMS-Verfahren ein Problem mit einem Prozess unter der Erf¨ llung dessen u Deadline immer planen, wenn (offensichtlich) die Ausf¨ hrungszeit kleiner gleich u der Deadline (hier auch Periode) ist. Interessanter ist der Fall f¨ r |V | → ∞. Dann u erh¨ lt man f¨ r die rechte Seite der Ungleichung (7.19) den Wert ln(2). Damit l¨ sst a u a sich die Aussage treffen, dass f¨ r alle Problemgr¨ ßen |V | immer ein g¨ ltiger Ab- u o u |V | laufplan gefunden wird, wenn ∑i:=1 δi /P(vi ) ≤ ln(2) gilt, d. h. wenn der Prozessor weniger als 1/ln2 · 100 % ≈ 69, 3 % ausgelastet ist. Man beachte, dass das Kriteri- um in Theorem 7.4.3 nat¨ rlich nur eine hinreichende Bedingung darstellt, so dass es u auch Probleminstanzen geben kann, f¨ r die der RMS-Algorithmus auch bei h¨ herer u o Prozessorauslastung einen Ablaufplan ﬁnden kann, der alle Deadlines einh¨ lt. a a ¨ Aus Ungleichung (7.19) l¨ sst sich ubrigens auch eine notwendige Bedingung f¨ r u |V | die Einhaltbarkeit aller Deadlines erkennen: ∑i:=1 δi /P(vi ) ≤ 1. Dies entspricht dem Grenzfall einer Prozessorauslastung von 100%. Falls diese Bedingung nicht erf¨ llt u ist, kann offensichtlich auch kein Algorithmus mit dynamischen Priorit¨ ten einen a g¨ ltigen Ablaufplan ﬁnden. u Damit stellt sich aber die Frage, ob es denn einen Algorithmus gibt, der auch |V | f¨ r den extremen Fall ∑i:=1 δi /P(vi ) = 1 einen g¨ ltigen Ablaufplan ﬁnden kann? Die u u Antwort heißt ja, und ein solcher Algorithmus ist der EDF-Algorithmus. Theorem 7.4.4 (Liu und Layland). Gegeben sei ein Ablaufplanungsproblem nach ∗ Deﬁnition 7.4.8 mit der Eigenschaft ∀vi ∈ V : τd (vi ) = P(vi ). Die Menge von Prozesse kann unter Erf¨ llung aller Deadlines mit dem EDF-Algorithmus geplant werden, u falls |V | δi ∑ P(vi ) ≤ 1 (7.20) i:=1 gilt. Der EDF-Algorithmus ist priorit¨ tsgesteuert mit dynamischer Priorit¨ t, wobei die a a h¨ chste Priorit¨ t demjenigen Prozess zugewiesen wird, dessen Deadline am kleinsten o a ist. Pr¨ emption erfolgt immer dann, wenn es einen noch nicht fertig abgearbeiteten a Prozess gibt, der eine h¨ here Priorit¨ t besitzt. o a Beispiel 7.4.7. Abbildung 7.32a) zeigt einen mit der EDF-Strategie ermittelten Ab- laufplan, der alle Deadlines f¨ r das Problem aus Beispiel 7.4.4 erf¨ llt. Dies gilt bei u u δi einer Prozessorauslastung von 100% (∑2 P(v ) = 1/2 + 2, 5/5 = 1). In Abb. 7.32b) i:=1 i
446 7 Software-Veriﬁkation ist ein Ablaufplan nach der RMS-Strategie dargestellt. EDF und RMS werden in der Praxis nahezu ausschließlich in der hier dargestellten pr¨ emptiven Version einge- a setzt. Antwortzeitanalyse Neben den vorgestellten einfachen auf Ressourcenauslastung beruhenden Tests in Gleichung (7.19) f¨ r RMS-Ablaufplanung und in Gleichung (7.20) f¨ r EDF, wur- u u ¨ den Tests entwickelt, die detailliertere Informationen uber das Zeitverhalten und Priorit¨ ten von Prozessen zur Bestimmung der Planbarkeit periodischer Prozesse a ausnutzen. F¨ r RMS betrachten Joseph und Pandya in [249] die Antwortzeit eines u Prozesses vi ∈ V im ung¨ nstigsten Fall gleicher Ankunftszeiten aller Prozesse. Die u Antworts- bzw. Flusszeit δF (vi ) ist dann durch die Summe der eigenen Ausf¨ hrungs- u zeit δi und der maximalen sog. Interferenz Ii gegeben. Der Interferenzterm Ii be- stimmt dabei die Summe der Verz¨ gerungszeiten, denen vi unterliegt, wenn dieser o durch h¨ herpriore Prozesse unterbrochen wird. Sei hp(vi ) ⊆ V die Menge h¨ herprio- o o ∗ rer Prozesse von vi und die Deadline td (vi ) gleich der Periode P(vi ) f¨ r alle vi ∈ V . u Dann gilt offensichtlich: δF (vi ) δF (vi ) := δi + ∑ δj P(v j ) ∗ ≤ td (vi ) = P(vi ) (7.21) v j ∈hp(vi ) ∗ Gibt es f¨ r diese rekursive Gleichung eine L¨ sung im Intervall [0, . . . ,td (vi )], so u o ∗ erf¨ llt der Prozess vi unter RMS-Ablaufplanung seine Deadline td (vi ). u Zeitgetriebene, dynamische Ablaufplanung Dynamische, priorit¨ tsbasierte Ablaufplanung stellt eine efﬁziente Methode zur Pla- a nung von Prozessen unter vielen m¨ glichen Umst¨ nden dar. Dies hat allerdings o a h¨ uﬁg zur Folge, dass das System bei dessen Ausf¨ hrung ein starkes dynamisches a u Verhalten zeigt, was die Analyse erschwert. Im Gegensatz dazu weist eine zeitge- triebene, dynamische Ablaufplanung jedem Prozess einen mehr oder weniger fest- stehenden Zeitschlitz f¨ r dessen Abarbeitung zu. Damit kann ein Prozess einen Pro- u zessor f¨ r ein genau festgelegtes Zeitbudget belegen. Wenn dieses Zeitbudget aufge- u braucht ist, wird dem n¨ chsten Prozess der Prozessor zugeteilt. Im Folgenden werden a zwei prominente Vertreter zeitgetriebener, dynamischer Ablaufplanung vorgestellt: Round-Robin- und TDMA-Ablaufplanung. Round-Robin-Ablaufplanung (RR) Bei der sog. Round-Robin-Ablaufplanung (RR) gibt es ein festes Zeitintervall Q, nach dessen Ablauf sp¨ testens ein Kontextwechsel eingeleitet wird (z. B. alle Q = a 100 Zeitschritte), falls nicht ein geplanter Prozess vor Ablauf des Zeitquantums be- endet wurde. Die laufbereiten Prozesse werden in einer zirkul¨ ren Warteschlange a verwaltet und reihum f¨ r die maximale Zeitdauer eines Zeitquantums geplant. u
7.4 Zeitanalyse 447 Beispiel 7.4.8. Betrachtet wird ein Problemgraph mit drei Prozessen v1 , v2 und v3 ohne Datenabh¨ ngigkeiten mit den Ausf¨ hrungszeiten δ1 := 24, δ2 := 3, δ3 := 30 und a u den Ankunftszeiten τr (v1 ) = τr (v2 ) = τr (v3 ) := 0. Abbildung 7.33 zeigt den mit der RR-Strategie gewonnenen Ablaufplan f¨ r ein Zeitquantum von Q := 4 Zeitschritten. u Man erkennt, dass zum Zeitpunkt τ = 4 der Knoten v1 suspendiert wird, da das Zeitquantum abgelaufen ist. Erst zum Zeitpunkt τ = 11 wird v1 weiter berechnet. Die mittlere Wartezeit betr¨ gt in diesem Beispiel δW = (47 − 24) + (7 − 3) + (57 − a 30)/3 = 18 Zeiteinheiten. CPU v1 v2 v3 v1 v3 v1 v3 v1 v3 v1 v3 v1 v3 v3 v3 0 4 8 12 16 20 24 28 32 36 40 44 48 52 56 τ Abb. 7.33. Ablaufplanung mit RR-Strategie Round-Robin-Ablaufplanung wird h¨ uﬁg in Mehrbenutzerbetriebssystemen an- a gewendet. Als Nachteil muss man h¨ uﬁg lange Wartezeiten in Kauf nehmen. Bei ei- a ner Anzahl von N planbaren Prozessen und einem Zeitquantum Q kann man jedoch die Schranke (N − 1)Q als l¨ ngstes Zeitintervall, bis ein Prozess sp¨ testens wieder a a weiter abgearbeitet wird, angeben. Falls Q gegen unendlich strebt, erh¨ lt man den a bekannten FCFS-Algorithmus (engl. First Come, First Served). Falls Q gegen null strebt, verh¨ lt sich das System (unter Vernachl¨ ssigung von Kontextwechselzeiten) a a wie ein System mit N Prozessoren, die allerdings jeweils nur die 1/N-fache Rechen- leistung besitzen. TDMA Neben der Round-Robin-Ablaufplanung gibt es eine weitere popul¨ re zeitgetriebe- a ne Ablaufplanungsstrategie, die als TDMA (engl. Time Division Multiple Access) bekannt ist. Hier werden jedem Prozess periodisch auf einem Prozessor Zeitslots zu- gewiesen. Im Gegensatz zur Round-Robin-Strategie erfolgt dies unabh¨ ngig davon, a ob der Prozess gerade laufbereit ist oder nicht. Damit h¨ ngt das Zeitverhalten eines a Prozesses nicht mehr vom Zeitverhalten anderer Prozesse ab, was die Zeitanalyse stark vereinfacht. Zum Beispiel l¨ sst sich die Antwortzeit eines Prozesses vi mit Pe- a riode P(vi ), zugewiesener Slotbreite S(vi ), Ausf¨ hrungszeit δi und Zeitquantum Q u wie folgt berechnen: δi δF (vi ) = δi + (Q − S(vi )) (7.22) S(vi ) δ Der eigenen Ausf¨ hrungszeit δi zuzuschlagen sind maximal S(vi ) Zeitscheiben, u i in denen vi die Ressource (Q − S(vi )) Zeitschritte nicht belegt. TDMA ist zwar im
448 7 Software-Veriﬁkation Bereich der Ablaufplanung auf Prozessoren wenig bekannt, wird hingegen oft zur Planung von Kommunikationen auf Bussen genutzt. 7.5 Literaturhinweise ¨ Die formale Aquivalenzpr¨ fung von Assemblerprogrammen auf Basis von symbo- u lischer Simulation ist in [122] beschrieben. Spezielle Eigenschaften zu Assembler- programmen f¨ r DSPs und VLIW-Prozessoren und deren Behandlung in der Aqui- u ¨ valenzpr¨ fung sind in [123] bzw. [159] aufgef¨ hrt. Der Einsatz von Schnittpunk- u u ¨ ten zur strukturellen Aquivalenzpr¨ fung von Assemblerprogrammen ist in [160] be- u ¨ ¨ schrieben. Eine Erweiterung der strukturellen Aquivalenzpr¨ fung zur Aquivalenz- u pr¨ fung von C-Programmen mit Hardware-Schaltungen ﬁndet sich in [161]. Weitere u Ans¨ tze zum Vergleich von C-Programmen mit Hardware sind in [270], [264] und a a ¨ [229] pr¨ sentiert. Die Aquivalenzpr¨ fung von C-Programmen auf Basis von symbo- u ¨ lischer Simulation ist in [315] beschrieben. In [394] ist die Aquivalenzpr¨ fung von u Schleifenprogrammen beschrieben. Weiterf¨ hrende Ans¨ tze sind in [395] und [396] u a vorgestellt. Die Verfahren zur funktions- und strukturorientierten Testfallgenerierung wer- den ausf¨ hrlich in [305] diskutiert. Bei den simulativen Veriﬁkationsmethoden ist ei- u ne 100%-ige Zweig¨ berdeckung heutzutage das Minimalkriterium in der Software- u Entwicklung. Der Standard DO-178B f¨ r die Software-Entwicklung in sicherheits- u kritischen Bereichen fordert beispielsweise einen modiﬁzierten Bedingungs-/Ent- scheidungs¨ berdeckungstest [382]. Darin werden Testf¨ lle gefordert, die zeigen, u a dass jede atomare Bedingung die Evaluierung einer Entscheidung unabh¨ ngig vona anderen atomaren Bedingungen beeinﬂussen kann. Eine vergleichende Studie zwi- schen Zweig-, Pfad- und strukturiertem Pfad¨ berdeckungstest ﬁndet sich in [227, u 228]. Ein modiﬁzierter strukturierter Pfad¨ berdeckungstest ist in [305] beschrieben. u a ¨ In diesem wird die Komplexit¨ t reduziert, indem die Uberdeckung von ausf¨ hrba- u ¨ ren Teilpfaden in Schleifen gefordert wird, nicht aber die Uberdeckung s¨ mtlicher a Kombinationen. Die datenﬂussorientierte Testfallgenerierung spielt in der Praxis heutzutage noch nicht die Rolle wie die kontrollﬂussorientierte Testfallgenerierung. Ein Vergleich der ¨ all defs-, all c-uses- und all p-uses-Uberdeckungstests ﬁndet sich in [190]. Dar¨ ber u ¨ hinausgehende Techniken sind beispielsweise der required k-tuples-Uberdeckungs- test [349, 109, 350] und der Datenkontext¨ berdeckungstest [290, 291, 109]. Letzterer u verlangt, dass alle existierenden M¨ glichkeiten den in einem gegebenen Grundblock o verwendeten Variablen Werte zuzuweisen, ber¨ cksichtigt werden. Dabei kann auch u die unterschiedliche Reihenfolge der Wertzuweisung ber¨ cksichtigt werden. u ¨ ¨ Eine gute Ubersicht uber Methoden und Werkzeuge zur formalen funktionalen Eigenschaftspr¨ fung von Programmen ﬁndet sich in [140]. Darin wird eine Unter- u scheidung in Verfahren zur statischen Programmanalyse, zur Modellpr¨ fung und zur u SAT-basierten Modellpr¨ fung vorgenommen. Die abstrakte Interpretation zur stati- u schen Programmanalyse wurde erstmal 1977 vorgestellt [118]. Die notwendigen ma- thematischen Zusammenh¨ nge zwischen konkretem und abstraktem Wertebereich, a
7.5 Literaturhinweise 449 unter denen der mittels abstrakter Interpretation berechnete abstrakte Fixpunkt eine korrekte Approximation des konkreten Fixpunktes ist, werden in [119] beschrieben. An gleicher Stelle ist beschrieben, wie abstrakte Wertebereiche nach Bedarf konstru- iert werden k¨ nnen. Bei den abstrakten Wertebereichen wird dabei zwischen relatio- o nalen und nichtrelationalen abstrakten Wertebereichen unterschieden. Die relatio- nalen DBM-Wertebereiche wurden zun¨ chst zur Analyse zeitbehafteter Petri-Netze a verwendet [471]. Eine h¨ here Expressivit¨ t besitzen Oktagon- [327] und Oktaeder- o a Wertebereiche [96]. Polyeder-Wertebereiche wurden erstmals zur Veriﬁkation num- merischer Eigenschaften von Programmen und des Zeitverhaltens eingebetteter Soft- ware verwendet [120, 213]. Ein weiteres großes Anwendungsgebiet statischer Pro- grammanalyse ist die Analyse von Programmen, die Zeiger verwenden. Die sog. Alias-Analyse untersucht, ob zwei Zeiger die selbe Speicherstelle adressieren. Die Ermittlung der Speicherstelle, auf die ein Zeiger zugreift, wird als engl. point to analysis bezeichnet [220]. Eine Generalisierung auf dynamisch erzeugte Datenstruk- turen erfolgt in [376, 248] und wird als engl. shape analysis bezeichnet. Die Zusammenh¨ nge und Unterschiede zwischen statischer Programmanalyse a und Modellpr¨ fung sind in [410, 389, 46] diskutiert. Werkzeuge zur Modellpr¨ fung u u von Software k¨ nnen generell in explizite und symbolische Modellpr¨ fer unterschie- o u den werden. Der wohl bekannteste Vertreter expliziter Modellpr¨ fer ist SPIN [222]. u Erste Versionen des Java Pathﬁnder haben auf SPIN aufgesetzt [456]. Neben SPIN und Java Pathﬁnder gibt es mit CMC [339], ZING [15] und VeriSoft [195] drei weite- re wichtige Vertreter expliziter Modellpr¨ fer. Letzterer ist zustandslos, d. h. besuchte u Zust¨ nde werden nicht gespeichert, und begegnet damit der Zustandsexplosion. Al- a lerdings ist dieses Verfahren unvollst¨ ndig f¨ r Systeme, die Zyklen enthalten. F¨ r a u u die Terminierung muss zus¨ tzlich die Suchtiefe beschr¨ nkt werden. a a Modellpr¨ fungsverfahren, die auf Abstraktionsverfeinerung beruhen, verwenden u zur Erstellung der abstrakten Modelle heutzutage Pr¨ dikatenabstraktion [205]. Ein a iteratives Verfahren zur Pr¨ dikatenabstraktion ist unter den Namen CEGAR (engl. a counterexample-guided abstraction reﬁnement) bekannt geworden [23, 100]. Die Entscheidungsprozeduren, die zur Bestimmung des abstrakten Modells ben¨ tigt wer- o den, basieren entweder auf Theoreml¨ sern [24, 131] oder SAT-Solvern [103, 114]. o Ein erstes Modellpr¨ fungsverfahren auf Basis von Pr¨ dikatenabstraktion mit dem u a Namen SLAM wurde von der Firma Microsoft entwickelt [25]. SLAM besteht aus mehreren Werkzeugen wie C2BP [26] zur Pr¨ dikatenabstraktion, dem symbolischen a Modellpr¨ fer BEBOP [27] sowie dem Simulations- und Verfeinerungswerkzeug u NEWTON [28]. W¨ hrend SLAM Theoreml¨ ser zur Pr¨ dikatenabstraktion einset- a o a zen, verwendet SATABS einen SAT-Solver [103]. F¨ r die eigentliche Veriﬁkation u setzt SATABS den QBF-Solver-basierten Modellpr¨ fer BOPPO [115] ein. u Eine der ersten Implementierungen eines SAT-basierten Modellpr¨ fers f¨ r C- u u Programme heißt CBMC, welches unterschiedliche Prozessor- und Speicherarchitek- turen unterst¨ tzt [104, 102]. Der Ansatz zur Zustandsraumreduktion durch Schleifen- u abwicklung geht auf Currie et al. zur¨ ck [123]. Die grundblockbasierte SAT-basierte u Modellpr¨ fung in [242] unterscheidet sich von BMC durch die Abstraktion vom u Programmz¨ hler, wodurch es u. a. leichter wird, Funktionsaufrufe zu modellieren. a Eine Erweiterung von CBMC auf SMT-Solver unter Verwendung von ganzzahliger
450 7 Software-Veriﬁkation linearer Arithmetik ist in [17, 18] beschrieben. Der einzige SAT-basierte Modell- pr¨ fungsansatz der ein Abrollen der Zustands¨ bergangsrelation vornimmt ist F-Soft u u [241]. WCET-Analyse im Allgemeinen ist nicht entscheidbar. Sowohl Kligerman and Stoyenko [263] als auch Puschner and Koza [368] haben die Bedingungen unter- sucht, unter denen das Problem entscheidbar wird. Zu diesen Bedingungen z¨ hlen a beschr¨ nkte Schleifen, Abwesenheit von rekursiven Funktionsaufrufen und Abwe- a senheit von dynamischen Funktionsaufrufen. Eine ILP-basierte WCET-Analyse ist in [302] vorgestellt. Eine Erweiterung um die Ber¨ cksichtigung eines Instruktions- u caches ist in [303] beschrieben. In [428] zeigen Theiling et al., dass es m¨ glich ist, o die Programmpfadanalyse von der Analyse der Zielarchitektur zu separieren, indem Ergebnisse der Zielarchitekturanalyse durch abstrakte Interpretation in dem ILP zur Bestimmung des l¨ ngsten Programmpfads verwendet werden. a Dynamische Ablaufplanungsverfahren und Echtzeitbedingungen sind ausf¨ hr- u lich in den B¨ chern [262], [308] und [79] pr¨ sentiert. Detaillierte Informationen u a ¨ uber EDF enth¨ lt das EDF-Buch [408]. In [468, 78] werden auch interessante Ver- a gleiche zwischen ratenmonotoner Ablaufplanung (RMS) und EDF beschrieben. Er- weiterungen der ratenmonotonen Ablaufplanung unter dem Namen deadlinemono- tone Ablaufplanung sind von Leung und Whitehead [301] sowie Lehoczky und Sha [300] betrachtet worden, wobei die Deadlines von Prozessen nicht notwendigerwei- se gleich ihrer Perioden sind. Joseph und Pandya entwickelten einen ersten Ansatz zur Antwortzeitanalyse bei ratenmonotoner Ablaufplanung [249]. Diese Antwort- zeitanalyse erlaubt die Betrachtung beliebiger Priorit¨ tszuweisungen. Er gilt daher a insbesondere auch im Falle der deadlinemonotonen Ablaufplanung, wenn die Dead- lines kleiner gleich den Perioden der Prozesse sind. F¨ r den Fall, dass Deadlines u gr¨ ßer als die Perioden eines Prozesses sein d¨ rfen, besteht das Problem, dass Instan- o u zen einer folgenden Iteration ankommen k¨ nnen, bevor die Ausf¨ hrung von Instan- o u zen der aktuellen Iteration beendet ist. Im Ansatz von Lehoczky [299] werden dazu Fenster von mehreren aufeinander folgenden Iterationen zusammen analysiert und daraus eine kombinierte Antwortzeit berechnet. Von Audsley [21] und Tindell [439] stammen schließlich Erweiterungen der Antwortzeitanalyse, die auch das Ph¨ nomena nicht exakt periodisch ankommender Prozesse, sondern sog. engl. release jitter zu- lassen sowie das Auftreten von periodischen sporadischen Prozessen, sog. engl. spo- radic bursts. F¨ r EDF-Ablaufplanung wird eine Antwortzeitanalyse in [406, 407] u beschrieben. Bei den zeitgetriebenen, dynamischen Ablaufplanungsverfahren sind die Round- Robin- und TDMA-Ablaufplanung die prominentesten Vertreter. Kopetz gibt in sei- ¨ ¨ nem Buch [266] eine gute Ubersicht uber TDMA-Ablaufplanung und der kommerzi- ellen Anwendung im sog. engl. Time-Triggered Protocol (TTP) [443]. Andere indus- trielle Anwendungen spiegeln sich wieder im sog. FlexRay-Busstandard [165]. Im Mittel f¨ hrt Round-Robin-Ablaufplanung zu besseren Ergebnissen, da bei TDMA u ungenutzte Zeitslots f¨ r andere Prozesse nicht zur Verf¨ gung stehen. Man kann zei- u u gen, dass Round-Robin-Ablaufplanung aber im schlechtesten Fall das Verhalten von TDMA besitzt. Daher kann man die TDMA-Analyse auch zur Analyse von Round- Robin-Ablaufplanung einsetzen.
8 Systemveriﬁkation System Modul Architektur Speziﬁkation Block Logik Implementierung ... Software Hardware Abb. 8.1. Veriﬁkation auf der Systemebene Der technologische Fortschritt erm¨ glicht es, Systeme mit einer immer gr¨ ße- o o ren Komplexit¨ t zu bauen. Um dabei mit den Entwurfsmethoden Schritt zu halten, a ist auch ein Schritt auf eine h¨ here Abstraktionsebene notwendig, die es erlaubt, o Systeme unabh¨ ngig von ihrer sp¨ teren Aufteilung in Hardware- und Software- a a Komponenten zu betrachtet. Diese Abstraktionsebene wird als Systemebene (engl. Electronic System Level) bezeichnet. Auf Systemebene wird das Systemverhalten oftmals als eine Menge kommuni- zierender Prozesse beschrieben. Insbesondere, wenn ausf¨ hrbare Verhaltensmodelle u zum Einsatz kommen, werden diese in zunehmenden Maße mit der Systembeschrei- bungssprache SystemC beschrieben. C. Haubelt, J. Teich, Digitale Hardware/Software-Systeme, eXamen.press, DOI 10.1007/978-3-642-05356-6 8, c Springer-Verlag Berlin Heidelberg 2010
452 8 Systemveriﬁkation Andererseits sind die Strukturmodelle auf Systemebene eine Netzliste aus Kom- ponenten mit der Granularit¨ t von Prozessoren, Hardware-Beschleunigern, Spei- a chern und Bussen. Auch diese Strukturmodelle werden zunehmend mit der System- beschreibungssprache SystemC modelliert. Von besonderem Interesse ist dabei die Interaktion der einzelnen Komponenten. Diese wird typischerweise als Transaktio- nen modelliert. Die resultierenden Modelle werden als Transaktionsebenenmodelle (engl. Transaction Level Models, TLMs) bezeichnet. Transaktionsebenenmodelle spielen bei der Veriﬁkation des Zeitverhaltens be- reits heutzutage eine zentrale Rolle. Der Grund hierf¨ r ist, dass TLMs aufgrund u der hohen Abstraktionsebene eine schnelle Simulation erm¨ glichen. Dabei liefern o sie bereits gute Absch¨ tzungen f¨ r nichtfunktionale Eigenschaften. Neben der Ver- a u besserung simulativer Verfahren zur Veriﬁkation des Zeitverhaltens, gab es in den letzten zehn Jahren enorme Fortschritte im Bereich der formalen Veriﬁkation des Zeitverhaltens auf der Systemebene. Im Folgenden werden Ans¨ tze zur Eigenschaftspr¨ fung auf der Systemebene a u behandelt. Dabei werden zun¨ chst formale Modellpr¨ fungsverfahren f¨ r SystemC- a u u Verhaltensmodelle pr¨ sentiert. Anschließend werden formale und simulative Ver- a fahren zur funktionalen Eigenschaftspr¨ fung von SystemC-Transaktionsebenenmo- u dellen vorgestellt. Zum Abschluss werden simulative und formale Methoden zur Zeitanalyse auf Systemebene diskutiert. ¨ 8.1 Funktionale Eigenschaftsprufung von SystemC-Modellen Im Folgenden werden Methoden zur funktionalen Eigenschaftspr¨ fung von Sys- u temC-Modellen vorgestellt. ¨ 8.1.1 Symbolische CTL-Modellprufung von SysteMoC-Modellen Dieser Abschnitt ist der symbolischen CTL-Modellpr¨ fung von SysteMoC-Modellen u (siehe Abschnitt 2.3.2) gewidmet. Die prinzipielle Vorgehensweise ist in [191] be- ¨ schrieben. Diese basiert auf Arbeiten uber symbolische Techniken f¨ r FunState- u Modelle, wie sie in [414] zusammengefasst sind. Im Folgenden wird zun¨ chst der a Zustandsraum eines SysteMoC-Modells genauer deﬁniert und dieser anschließend mit Hilfe von Intervall-Entscheidungsdiagrammen symbolisch repr¨ sentiert. Die a symbolische Modellpr¨ fung wird anschließend diskutiert. u Repr¨ sentation des Zustandsraums a F¨ r die sp¨ ter vorgestellte symbolische CTL-Modellpr¨ fung wird eine symboli- u a u sche Darstellung von Zust¨ nden und Zustands¨ berg¨ ngen von SysteMoC-Modellen a u a ben¨ tigt. Aufgrund der Komplexit¨ t von SysteMoC-Modellen wird bei der Re- o a pr¨ sentation der Zustandsr¨ ume eine Abstraktion auf das zugrundeliegende FunState- a a Modell betrachtet. Dabei werden Datenwerte nicht ber¨ cksichtigt. Der (abstrakte) u
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 453 Zustand eines SysteMoC-Modells ist dann durch die momentanen Zust¨ nde der end- a lichen Automaten der Aktoren im SysteMoC-Modell und die F¨ llst¨ nde der Kan¨ le u a a gegeben. Regul¨ re Zustandsautomaten a Der abstrakte Zustandsraum eines SysteMoC-Modells ist aufgrund der unbeschr¨ nk- a ten FIFO-Kan¨ le potentiell unendlich groß. Eine endliche Repr¨ sentation des Zu- a a u ¨ standsraums f¨ r SysteMoC-Modelle kann allerdings uber sog. Regul¨ re Zustandsau- a tomaten (engl. Regular State Machines, RSMs) [434] erreicht werden. RSMs sind daf¨ r geeignet, regul¨ re Zustands¨ nderungen von nebenl¨ uﬁgen Kon- u a a a troll- und/oder Datenﬂussmodellen (unter anderem Petri-Netze, FunState- und Sys- teMoC-Modellen) zu beschreiben. Dabei k¨ nnen RSMs bestimmte Klassen von un- o endlichen Zustandssystemen modellieren und erweitern die Klasse der endlichen Au- tomaten. RSMs werden hier lediglich in einer eingeschr¨ nkten Form vorgestellt und a ¨ uber ihre graphischen Repr¨ sentationen als statische und dynamische Zustands¨ ber- a u gangsdiagramme eingef¨ hrt. Erweiterungen sind in [434] zu ﬁnden. u Deﬁnition 8.1.1 (Statisches Zustandsdiagramm einer RSM). Ein statisches Zu- stands¨ bergangsdiagramm ist ein gerichteter Graph G = (V, E, D, P, v0 , I0 ) mit u • einer Menge von Knoten V , • einer Menge gerichteter Kanten E ⊆ V ×V , • einer Funktion D : E → Zm , die jeder Kante e = (vi , v j ) ∈ E einen Distanzvektor ganzer Zahlen d(e) = d(vi , v j ) ∈ Zm der Dimension m zuordnet, • einer Pr¨ dikatenfunktion P : E × Zm → B, die jeder Kante e ∈ E ein Pr¨ dikat a a P(e, I) zuordnet und • einem Knoten v0 ∈ V und einem Vektor I0 ∈ Zm , die den Anfangszustand bilden. Das statische Zustands¨ bergangsdiagramm ist eine abk¨ rzende Schreibweise u u f¨ r das m¨ glicherweise unendliche, dynamische Zustands¨ bergangsdiagramm einer u o u RSM. Das dynamische Zustands¨ bergangsdiagramm ergibt sich, indem die Zust¨ nde u a des statischen Zustands¨ bergangsdiagramms an jeden g¨ ltigen Indexpunkt, der sich u u aus den Distanzvektoren unter Ber¨ cksichtigung der Pr¨ dikate ergibt, kopiert wer- u a den, und anschließend die Zustands¨ berg¨ nge entsprechend zwischen den Zust¨ nden u a a und Indexpunkten eingetragen werden. ¨ Deﬁnition 8.1.2 (Dynamisches Zustandsubergangsdiagramm einer RSM). Das dynamische Zustands¨ bergangsdiagramm Gd = (X, T, x0 ) eines gegebenen stati- u schen Zustands¨ bergangsdiagramms G = (V, A, D, P, v0 , I0 ) ist ein unendlicher, ge- u richteter Graph, der wie folgt deﬁniert ist: • Die Knoten x ∈ X repr¨ sentieren (dynamische) Zust¨ nde des dynamischen Zu- a a stands¨ bergangsdiagramms. Es gilt X = V × Zm mit der Indexmenge des dyna- u mischen Zustands¨ bergangsdiagramms Zm . Der Knoten x = (v, I) ∈ X bezeich- u net den Zustand f¨ r einen Knoten v ∈ V eines statischen Zustands¨ bergangsdia- u u gramms und einen Indexpunkt I ∈ Zm .
454 8 Systemveriﬁkation • Der Zustand x0 = (v0 , I0 ) ist der Anfangszustand des dynamischen Zustands¨ ber- u gangsdiagramms. • Die Kanten T stellen (dynamische) Transitionen des dynamischen Zustands¨ ber- u gangsdiagramms dar. Es gibt eine Kante t = (x1 , x2 ) ∈ T von Zustand x1 = (v1 , I1 ) ∈ X zu Zustand x2 = (v2 , I2 ) ∈ X, genau dann, wenn e = (v1 , v2 ) ∈ A, I2 − I1 = d(v1 , v2 ) und P(e, I1 ) = T gilt. ¨ Damit lassen sich RSMs mit einer f¨ r Transitionssysteme ublichen Semantik deﬁ- u nieren. Deﬁnition 8.1.3 (Semantik einer RSM). Das Verhalten eines regul¨ ren Zustands- a automaten mit einem dynamischen Zustands¨ bergangsdiagramm Gd = (X, T, x0 ) ist u wie folgt deﬁniert: • Anfangs ist der regul¨ re Zustandsautomat im Zustand x0 . a t • Eine Transition x1 −→ x2 ver¨ ndert den Zustand einer RSM von x1 ∈ X zu x2 ∈ X, a wobei t = (x1 , x2 ) ∈ T nichtdeterministisch aus allen Transitionen t mit Anfangs- zustand x1 gew¨ hlt wird. a Mit einem Pfad durch ein dynamisches Zustands¨ bergangsdiagramm ist eine u konkrete Folge von dynamischen Zust¨ nden und Transitionen gemeint, die eindeutig a von einem Indexpunkt in dem dynamischen Zustands¨ bergangsdiagramm zu einem u anderen Indexpunkt f¨ hrt. u Beispiel 8.1.1. Abbildung 8.2a) zeigt ein statisches Zustands¨ bergangsdiagramm. u Das entsprechende dynamische Zustands¨ bergangsdiagramm ist in Abb. 8.2b) darge- u stellt. An den Kanten des statischen Zustands¨ bergangsdiagramms ist der jeweilige u Distanzvektor annotiert und, falls vorhanden, ein Pr¨ dikat vorangestellt (abgetrennt a mit /). Repr¨ sentation von SysteMoC-Modellen als RSMs a Um den abstrakten Zustandsraum eines SysteMoC-Modells (N, M, I, O) mit Netz- graph (A,C, E) (siehe Deﬁnition 2.3.1 auf Seite 68) als RSM zu repr¨ sentieren, wird a im Folgenden gezeigt, wie ein statisches Zustands¨ bergangsdiagramm nach Deﬁni- u tion 8.1.1 f¨ r ein gegebenes SysteMoC-Modell aufgebaut wird. Der abstrakte Zu- u standsraum eines SysteMoC-Modells setzt sich aus 1. den m¨ glichen Zust¨ nden der endlichen Automaten aller SysteMoC-Aktoren o a und 2. den m¨ glichen FIFO-F¨ llst¨ nden zusammen. o u a In einem ersten Schritt wird deshalb der Produktautomat Mp mit Zustandsmen- ge Q p und Zustands¨ bergangsrelation R p aller endlichen Automaten der Aktoren im u SysteMoC-Modell gebildet. Basierend auf dem Produktautomaten kann anschlie- ßend das statische Zustands¨ bergangsdiagramm G = (V, E, D, P, v0 , I0 ) wie folgt ge- u bildet werden:
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 455 a) b) i1 −1 i1 ≥ 1/ 0 i2 0 1 1 i2 ≥ 1/ −1 0 0 1 I0 = 1 Abb. 8.2. a) statisches und b) dynamisches Zustands¨ bergangsdiagramm [414] u • Die Menge der Knoten V ist die Menge der Zust¨ nde Q p . a • Die Kanten E sind die Zustands¨ bergangsrelationen in R p , also ∀ei = (q, q ) ∈ u E : ∃(q, q ) ∈ R p . • Die Dimension m der Distanzvektoren aus Zm entspricht der Anzahl der Kan¨ le a in dem SysteMoC-Modell, also m = |C|. • Die Funktion D kann aus den Attributen der Zustands¨ berg¨ nge (q, q ) ∈ R p ex- u a trahiert werden, indem aus den Konsumptions- und Produktionsraten des Zu- stands¨ bergangs f¨ r die Kante ei = (q, q ) ∈ E der Distanzvektor f¨ r die Kante u u u bestimmt wird. Dabei werden Produktionsraten zu positiven Elementen des Vek- tors und Konsumptionsraten zu negativen Elementen. Nicht beteiligte Kan¨ le er- a halten darin den Wert null. • Die Pr¨ dikate P(e, I) werden so gew¨ hlt, dass kein Indexpunkt mit negativen a a Elementen und kein Indexpunkt, der in einem Element die Kanalbeschr¨ nkunga verletzt, erreicht werden kann. • Anfangszustand v0 ist der aus allen Anfangszust¨ nden des endlichen Automaten a der Aktoren zusammengesetzte Zustand. • Der Anfangsindexpunkt I0 wird aus der Anfangsmarkierung der Kan¨ le be- a stimmt. Beispiel 8.1.2. Abbildung 8.3 zeigt ein SysteMoC-Modell und das daraus konstru- ierte statische Zustands¨ bergangsdiagramm. In dem SysteMoC-Modell wird durch u jede Transition eine Marke von Kanal c1 nach Kanal c2 verschoben, der rechte Aktor kann dabei je nach Ergebnis von fcheck auch seinen Zustand wechseln. Die Kan¨ le a c1 und c2 haben jeweils die Kapazit¨ t von acht Marken und beinhalten jeweils ei- a ne Marke im Anfangszustand. Da der linke Aktor lediglich einen Zustand besitzt,
456 8 Systemveriﬁkation enth¨ lt der Produktautomat lediglich zwei Zust¨ nde. In den Pr¨ dikaten an den Zu- a a a stands¨ berg¨ ngen bezeichnen c1 # bzw. c2 # die im Kanal c1 bzw. Kanal c2 verf¨ gbare u a u Anzahl an Marken. a) o1 c1 i1 i2 (1)&o1 (1) i1 (1)&o2 (1)&¬ fcheck s0 i1 (1)&o2 (1) s0 s1 i1 (1)&o2 (1) c2 i1 (1)&o2 (1)& fcheck i2 o2 b) c1 # ≥ 1 ∧ c2 # < 8 ∧ ¬ fcheck / −1 1 1 1 c1 # < 8 ∧ c2 # ≥ 1/ c1 # < 8 ∧ c2 # ≥ 1/ −1 −1 s0 , s 0 s0 , s1 −1 −1 c1 # ≥ 1 ∧ c2 # < 8/ c1 # ≥ 1 ∧ c2 # < 8/ 1 c1 # ≥ 1 ∧ 1 c2 # < 8 ∧ fcheck / 1 −1 I0 = 1 1 Abb. 8.3. a) SysteMoC-Modell und b) zugeh¨ riges statisches Zustands¨ bergangsdiagramm o u [193] Symbolische Repr¨ sentation des Zustandsraums a Es ist denkbar auf der Repr¨ sentation von regul¨ ren Zustandsautomaten eine ex- a a plizite CTL-Modellpr¨ fung zu implementieren (siehe Abschnitt 5.2). Efﬁzienter u sind allerdings symbolische Verfahren, also Verfahren, die auf einer impliziten Re- pr¨ sentation des Zustandsraums basieren (siehe auch Abschnitt 5.3). W¨ hrend es a a zun¨ chst scheint, dass ROBDDs eine m¨ gliche symbolische Repr¨ sentation des Zu- a o a standsraums f¨ r SysteMoC-Modelle darstellen, kommen diese bei einer genauen u Betrachtung nicht mehr in Frage. Die potentiell unbeschr¨ nkten FIFO-Kan¨ le im a a SysteMoC-Modell, die einen potentiell unendlichen Zustandsraum aufspannen, las- sen sich durch BDDs nicht repr¨ sentieren. a Aus diesem Grund werden im Folgenden sog. Intervall-Entscheidungsdiagramme (engl. Interval Decision Diagram, IDD) zur symbolischen Repr¨ sentation des Zu- a standsraums f¨ r SysteMoC-Modelle betrachtet. Neben IDDs wird eine zweite Klas- u se von Intervalldiagrammen ben¨ tigt, die sog. Intervall-Abbildungsdiagramme (engl. o Interval Mapping Diagram, IMD), um Zustands¨ berg¨ nge symbolisch zu repr¨ sen- u a a tieren. IDDs und IMDs bilden zusammen die Grundlage f¨ r efﬁziente symboli- u sche Verfahren wie Modellpr¨ fung auf einer Vielzahl von Berechnungsmodellen, u
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 457 z. B. Prozessnetzwerke [415], Petri-Netze [416] und FunState-Modelle [414] oder f¨ r symbolische Ablaufplanung von FunState- [418, 414] und SysteMoC-Modellen u [192]. IDDs und IMDs werden im Folgenden mit der Beschr¨ nkung auf ganzzahlige a Intervalle eingef¨ hrt (siehe auch [414, 193]). u Intervall-Entscheidungsdiagramme (IDDs) Intervall-Entscheidungsdiagramme (IDDs) erlauben die Darstellung von Funktio- nen mit n Variablen und einem diskreten, endlichen Deﬁnitionsbereich. Weite- re notwendige Eigenschaften der Funktionen werden weiter unten diskutiert. Sei f (x1 , x2 , ..., xn ) eine Funktion mit f : A1 × A2 × ... × An → B, mit Ai ⊆ Z f¨ r die u Deﬁnitionsbereiche aller xi und B ⊂ Z, wobei die M¨ chtigkeit von B endlich ist. Va- a riablen in Ai seien Intervalle auf Z, dargestellt mit [al , au ]. Dabei bezeichnet al die untere Schranke und au die obere Schranke des geschlossenen Intervalls. Das ge- schlossene Intervall enth¨ lt sowohl al als auch au . Intervalle, bei denen eine oder a beide Grenzen unendlich bzw. minus unendlich sind, werden als halboffene oder of- fene Intervalle bezeichnet. Das Zeichen ∞ wird f¨ r eine unendliche obere Schranke, u das Zeichen −∞ f¨ r eine unendliche untere Schranke eingesetzt. Offene Enden ei- u nes Intervalls werden durch ( bzw. ) gekennzeichnet, z. B. (−∞, au ). In diesem Fall enth¨ lt das Intervall weder −∞ noch au . a Deﬁnition 8.1.4 (Intervalluberdeckung). Die Menge Δ (Ai ) = {Δ1 , Δ2 , . . . , Δ |Δ (Ai )| } ¨ aus |Δ (Ai )| Teilintervallen Δ j nennt man Intervall¨ berdeckung von Ai , genau dann, u wenn jedes Δ j ein Teilintervall von Ai ist, d. h. Δ j ⊆ Ai , und Δ (Ai ) vollst¨ ndig ist, a d. h. Ai = Δ j ∈Δ (Ai ) Δ j erf¨ llt ist. u Eine Intervall¨ berdeckung eines Deﬁnitionsbereichs deckt diesen also exakt und u ¨ l¨ ckenlos ab, erlaubt aber Uberschneidungen der Intervalle. Eine disjunkte Inter- u ¨ vall¨ berdeckung verbietet genau diese Uberschneidungen. Mit anderen Worten: Je- u des Element aus Ai muss in genau einem Teilintervall der Intervallpartition Δ (Ai ) enthalten sein. ¨ Deﬁnition 8.1.5 (Disjunkte Intervalluberdeckung). Gegeben sei eine Intervall- uberdeckung Δ (Ai ). Δ (Ai ) heißt disjunkt oder auch Intervallpartition, genau dann, ¨ wenn ∀1 ≤ s,t ≤ |Δ (Ai )|, s = t : Δ s ∩ Δt = ∅ gilt. Gegeben sei eine Funktion f und ein Intervall Δ j ∈ Δ (Ai ). Der Kofaktor bez¨ glich u xi sei bezeichnet durch f |xi :=b (x1 , x2 , . . . , xn ) = f (x1 , x2 , . . . , xi−1 , b, xi+1 , . . . , xn ). Falls f¨ r alle Belegungen von xi aus dem Intervall Δ j gilt, dass ∀b, c ∈ Δ j : f |xi :=b = f |xi :=c u ist, so sagt man, dass f unabh¨ ngig von xi ∈ Δ j ist. Der zugeh¨ rige Kofaktor wird mit a o f |xi :∈Δ j bezeichnet. Das Intervall Δ j wird dann als Unabh¨ ngigkeitsintervall (engl. a Independence Interval, II) von f in Bezug auf xi bezeichnet. Sind alle Teilintervalle einer Intervallpartition Δ (Ai ) Unabh¨ ngigkeitsintervalle, heißt Δ (Ai ) Unabh¨ ngig- a a keitsintervallpartition (engl. Independence Interval Partition, IIP). Intervalle heißen schließlich benachbart, wenn sie zu einem einzelnen Intervall zusammengefasst werden k¨ nnen. Dabei d¨ rfen die Intervalle auch uberlappen. o u ¨
458 8 Systemveriﬁkation Deﬁnition 8.1.6 (Reduzierte Intervallpartition). Gegeben sei ein IIP Δ (Ai ) = {Δ 1 , Δ2 , . . . , Δ|Δ (Ai )| }. Δ (Ai ) heißt genau dann minimal, wenn sie keine benachbarten Teil- intervalle enth¨ lt, die zu einem Unabh¨ ngigkeitsintervall zusammengefasst werden a a k¨ nnen. Δ (Ai ) heißt geordnet, genau dann, wenn alle oberen Schranken aller Teilin- o tervalle in Bezug auf ihren Index der Gr¨ ße nach aufsteigend geordnet sind. Ein IIP, o das minimal und geordnet ist, heißt reduziert. Ein reduziertes IIP einer Funktion ist eindeutig [414]. Das folgende Beispiel il- lustriert die obigen Deﬁnitionen. Es stammt aus [414] Beispiel 8.1.3. Gegeben ist die folgende Funktion [0,3] [0,5] [4,5] [6,∞) [0,7] f (x1 , x2 , x3 ) := F falls x1 ∧ x2 ∨ x1 ∨ x1 ∧ x3 T sonst Der Ausdruck x[al ,au ] ist ein Literal einer Variablen x in Bezug auf das Intervall [al , au ] und wird durch folgende Funktion deﬁniert (siehe auch Anhang B.1): F wenn x ∈ [al , au ] x[al ,au ] = T wenn x ∈ [al , au ] Der Deﬁnitionsbereich f¨ r x1 , x2 , x3 ist A1 = A2 = A3 = [0, ∞). Die Wertemenge der u Funktion f ist B = {F, T} = B. Der Kofaktor f |x1 :∈[4,5] (x1 , x2 , x3 ) ist gleich F. Die Intervalle [0, 7] und [4, 5] sind Unabh¨ ngigkeitsintervalle der Funktion f bez¨ glich der Variablen x3 . Dies gilt je- a u doch nicht f¨ r das Intervall [6, 9]. Die Menge Δ (A1 ) = {Δ 1 , Δ 2 , Δ 3 } mit Δ 1 = [0, 3], u Δ2 = [4, 5] und Δ3 = [6, ∞) ist eine Intervallpartition. F¨ r f ist Δ (A1 ) eine reduzierte u IIP. Darstellung von IDDs IDDs k¨ nnen, wie andere Entscheidungsdiagramme, graphisch dargestellt werden o (siehe Anhang B.1). Sie dienen der Repr¨ sentation von mehrwertigen Funktionen, a welche sich mit Hilfe von Intervallpartitionen mit endlich vielen Unabh¨ ngigkeits- a intervallen zerlegen lassen. Deﬁnition 8.1.7 (IDD). Ein Intervall-Entscheidungsdiagramm (IDD) f¨ r eine Funk- u tion f : A1 , . . . , An → B ist ein gerichteter azyklischer Graph G = (V, E) mit Knoten- menge V und Kantenmenge E sowie den folgenden Eigenschaften: • G ist ein Baum, • V ist eine Partition von Terminalknoten VT und Nichtterminalknoten VN , • eine Funktion index : VN → {1, . . . , n} weist jedem Nichtterminalknoten v ∈ VN eine Variablen xindex(v) zu, • alle Intervallpartitionen Δ (Aindex(v) ) = {Δ1 , Δ2 , . . . , Δ|Δ (Aindex(v) )| } sind IIP, • f¨ r jeden Nichtterminalknoten v ∈ VN weist eine Funktion child : VN × {1, . . . , u |Δ (Aindex(v) )|} → V dem Knoten v seine Nachfolger zu, d. h. (v, child(v, k)) ∈ E, mit 1 ≤ k ≤ |Δ (Aindex(v) )|,
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 459 • eine Funktion value : VT → B weist jedem Terminalknoten einen Wert aus der Zielmenge B zu. ¨ Bei Entscheidungsdiagrammen werden Funktionen als aquivalent zu ihrem zu- geh¨ rigen Knoten betrachtet. Eine Funktion fv mit zugeh¨ rigem Knoten v und Index o o index(v) kann auch als (|Δ (Aindex(v) )| + 1)-Tupel dargestellt werden: f v = (xindex(v) , (Δ1 , F1 ), . . . , (Δ |Δ (Aindex(v) )| , F|Δ (Aindex(v) )| )) (8.1) Dabei besteht jedes Paar (Δk , Fk ) aus einem Intervall Δk der Intervallpartition Δ (Ai ) und einer Funktion Fk beziehungsweise dem dieser zugeh¨ rigem Knoten child(v, k). o Die Funktion fv mit zugeh¨ rigem Knoten v ∈ V wird rekursiv deﬁniert: o • Ist v ein Terminalknoten, so gilt f v := value(v). • Ist v ein Nichtterminalknoten mit Index index(v), dann ist der Wert von f v gege- ben durch die Boole-Shannon Zerlegung Δ f v := xindex(v) ∧ fchild(v, j) j Δ j ∈Δ (Aindex(v) ) Die Argumente einer Funktion beschreiben also einen Pfad durch das zugeh¨ rige o IDD. Der Pfad beginnt bei dem Quellknoten und endet in einem Terminalknoten, der dem Funktionswert entspricht. Die durch das IDD darzustellende Funktion f ist dem Quellknoten des IDD zugeordnet. Beispiel 8.1.4. Das IDD f¨ r die Funktion aus Beispiel 8.1.3 ist in Abb. 8.4 zu sehen. u x1 [0, 3] [6, ∞) x2 [4, 5] [6, ∞) x3 [0, 5] [8, ∞) [0, 7] F T Abb. 8.4. Intervall-Entscheidungsdiagramm f¨ r die Funktion f aus Beispiel 8.1.3 [414] u
460 8 Systemveriﬁkation Um eine kanonische Darstellung von Funktionen durch IDDs zu erreichen, wird eine Variablenordnung ben¨ tigt. Ein IDD heißt geordnet (engl. Ordered Interval De- o cision Diagram, OIDD), genau dann, wenn auf jedem Pfad vom Quellknoten zu einem Terminalknoten die Variablen in der selben Reihenfolge auftreten. Ein OIDD heißt reduziert (engl. Reduced Ordered Interval Decision Diagram, ROIDD), genau dann, wenn 1. jeder Nichtterminalknoten v ∈ VN mindestens zwei voneinander verschiedene Nachfolger besitzt, 2. er nicht zwei unterschiedliche Knoten v und v enth¨ lt, die Quellknoten von iso- a morphen Teilgraphen sind, und 3. die IIPs Δ (Aindex(v) ) aller Nichtterminalknoten v ∈ VN reduziert sind. Zwei Teilgraphen eines IDD mit Quellknoten v, v ∈ V und v = v heißen isomorph, wenn die durch sie repr¨ sentierten Funktionen aquivalent sind, also fv ≡ fv gilt. a ¨ ¨ Isomorphe Teilgraphen k¨ nnen, ahnlich zu ROBDDs, in der Darstellung zusammen- o gefasst werden. Um ein OIDD zu reduzieren, werden folgende Reduktionsregeln angewendet: 1. Elimination: Wenn alle ausgehenden Kanten eines Nichtterminalknotens v ∈ VN in dem gleichen Knoten v enden, wird Knoten v entfernt und alle vorher in v eingehenden Kanten zeigen auf v . 2. Verschmelzung: Wenn unterschiedliche Nichtterminalknoten mit gleichem Index und gleicher Intervallpartition existieren, und diese jeweils die gleichen Nach- folger haben (oder wenn unterschiedliche Terminalknoten v ∈ VT mit gleichem Wert existieren), werden all diese bis auf einen Knoten entfernt und deren ein- gehende Kanten zeigen auf den verbleibenden Knoten. 3. Normalisierung: Wenn eine IIP eines Nichtterminalknotens v ∈ VN nicht mini- mal und geordnet ist, muss diese reduziert werden. Daf¨ r werden die Teilinter- u valle und ihre zugeh¨ rigen Nachfolger geordnet. Kanten aus v mit benachbarten o Intervallen, die im gleichen Nachfolger enden, werden durch eine Kante ersetzt, die alle diese benachbarten Intervalle zusammenfasst. Die Reduktionsregeln 1. und 2. sind in Abb. 8.5 dargestellt. F¨ r alle xi gilt der u Deﬁnitionsbereich Ai = [0, ∞). Strehl und Thiele beweisen in [415], dass ROIDDs eine kanonische Darstellung f¨ r mehrwertige Funktionen sind, welche sich mit Hil- u fe von Intervallpartitionen mit endlich vielen Unabh¨ ngigkeitsintervallen zerlegen a lassen. Intervall-Abbildungsdiagramme F¨ r die Manipulation von IDDs werden sog. Intervall-Abbildungsdiagramme (engl. u Interval Mapping Diagrams, IMDs) verwendet. Bevor diese formal eingef¨ hrt wer- u den, wird eine einfache Intervallarithmetik als Grundlage pr¨ sentiert. Mit dieser a k¨ nnen beispielsweise zwei nichtleere Intervalle addiert oder subtrahiert werden. Die o Argumente und das Ergebnis dieser Operationen sind jeweils Intervalle aus Z. Die ¨ Deﬁnitionen zeigen der Ubersicht halber nur geschlossene Intervalle.
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 461 a) b) x1 x1 x1 x1 x1 [0, 1] [0, 1] [0, 1] [0, 1] [0, 1] [2, ∞) [2, ∞) [2, ∞) x2 x2 x2 [0, 1] [2, ∞) x3 x3 x3 x3 x3 x3 Abb. 8.5. Reduktionsregeln f¨ r Intervall-Entscheidungsdiagramm [193] u Deﬁnition 8.1.8 (Intervalladdition). Die Addition zweier Intervalle [a, b] und [c, d] ist deﬁniert als [a, b] + [c, d] = [a + c, b + d]. Das aus der Addition resultierende Intervall enth¨ lt also alle Zahlen, die durch Ad- a dition von einer beliebigen Zahl aus dem ersten Intervall zu einer beliebigen Zahlen aus dem zweiten Intervall resultieren k¨ nnen. o Deﬁnition 8.1.9 (Intervallsubtraktion). Die Subtraktion zweier Intervalle [a, b] und [c, d] ist deﬁniert als [a, b] − [c, d] = [a, b] + [−d, −c]. Das Ergebnis der Subtraktion zweier Intervalle ist ein Intervall, das alle Zahlen enth¨ lt, die durch Subtraktion einer beliebigen Zahl aus dem Intervall [c, d] von einer a beliebigen Zahl aus dem Intervall [a, b] resultieren k¨ nnen. o IMDs werden durch sog. Abbildungsgraphen graphisch repr¨ sentiert. a Deﬁnition 8.1.10 (Abbildungsgraph). Ein Abbildungsgraph ist ein azyklischer ge- richteter Graph G = (V, E) mit ausgezeichnetem Quellknoten. Die Menge der Knoten V ist in zwei Partitionen eingeteilt, die Nichtterminalknoten VN und die Terminal- knoten VT . Jeder Nichtterminalknoten v ∈ VN hat einen Index index(v), eine Menge von Intervall-Abbildungsfunktionen func(v) = { f1 , f2 , . . . , f n } und |func(v)| Nach- folger, bezeichnet als child(v, k) ∈ V mit 1 ≤ k ≤ |func(v)|. Die Abbildungsfunktionen fk (v) ∈ func(v) sind mit den entsprechenden Kanten (v, child(v, k)) ∈ E assoziiert. Es gibt genau einen Terminalknoten v ∈ VT mit dem Wert value(v) = T. Eine Intervall-Abbildungsfunktion f : I → I bildet Intervalle auf Intervalle ab, wobei I die Menge aller Intervalle aus Z beschreibt. Eine Intervall-Abbildungs- funktion f (Δ ) = Δ , die ein Intervall auf sich selbst abbildet, wird als neutral be- zeichnet. IMDs k¨ nnen verwendet werden, um IDDs zu manipulieren. Dabei m¨ ssen o u ¨ beide Diagramme die gleiche Variablenordnung verwenden. F¨ r die Ubergangsbe- u schreibung von SysteMoC-Modellen wird eine eingeschr¨ nkte Klasse von IMDs ver- a wendet. Diese werden als engl. Predicate Action Diagrams (PADs) bezeichnet. Deﬁnition 8.1.11 (PAD). Ein Predicate Action Diagram (PAD) ist ein IMD, das nur zwei Arten von Intervall-Abbildungsfunktionen verwendet:
462 8 Systemveriﬁkation Δ ∩ ΔP + ΔA falls Δ ∩ ΔP = ∅ f + (Δ ) := [] sonst und ΔA falls Δ ∩ ΔP = ∅ f := (Δ ) := [ ] sonst f+ wird Versetzungs- und f:= Zuweisungsfunktion genannt. Jeder Abbildungsfunk- tion sind zwei w¨ hlbare Intervalle zugeordnet, das Pr¨ dikatenintervall ΔP und das a a Aktionsintervall ΔA . Im Folgenden werden PADs als IMDs bezeichnet. Die Versetzungs- und Zuwei- sungsfunktion schneiden erst das Argumentintervall Δ mit ihrem Pr¨ dikatenintervall a ΔP . Ist die Schnittmenge leer, ist das Resultat der Funktionen das leere Intervall. Ansonsten liefert die Versetzungsfunktion ein Intervall, das aus der Addition der Schnittmenge mit dem Aktionsintervall Δ A der Funktion resultiert. Die Zuweisungs- funktion ergibt bei einer nichtleeren Schnittmenge immer ihr Aktionsintervall. Die Abbildungsfunktionen eines IMD werden also ausschließlich durch zwei Intervalle als Parameter vollst¨ ndig beschrieben. a F¨ r die Versetzungsfunktion f + wird im Folgenden die Notation Δ P /+Δ A und u f¨ r die Zuweisungsfunktion f:= die Notation Δ P /:= ΔA verwendet. Ein Versetzen u von Intervallen in negative Richtung ist mit der Versetzungsfunktion auch m¨ glich. o Soll um ein Intervall Δ A = [a, b] in negative Richtung versetzt werden (Intervall- subtraktion), wird das durch Addition von [−b, −a] erreicht. Dies wird auch als ΔP /−ΔA geschrieben. F¨ r eine Variable xi ist die Abbildungsfunktion ΔP /+[0, 0] u mit ΔA = Ai neutral. Eine allgemeine neutrale Zuweisungsfunktion existiert nicht. Abbildung 8.6b) zeigt ein Beispiel f¨ r ein IMD mit drei Variablen. u a) x1 b) x1 [2, ∞)/−[1, 2] [0, ∞)/+[1, 4] [0, ∞) x2 x2 x2 [0, 0] [1, 2] [1, ∞)/−[1, 1] [1, ∞)/+[1, 1] x3 x3 x3 x3 [0, ∞) [0, 0] [0, ∞)/+[1, 3] [2, ∞)/−[2, 2] T T Abb. 8.6. a) Intervall-Entscheidungsdiagramm ohne Kanten zum Terminalknoten mit Wert F und b) Intervall-Abbildungsdiagramm [414] Im Gegensatz zu IDDs ist bei IMDs im Allgemeinen keine kanonische Darstel- lung m¨ glich. Dennoch k¨ nnen h¨ uﬁg, abh¨ ngig von der Struktur der repr¨ sentierten o o a a a
8.1 Funktionale Eigenschaftspr¨ fung von SystemC-Modellen u 463 Funktion, Reduktionsregeln f¨ r IMDs angeben werden. Die sp¨ ter f¨ r die Modell- u a u pr¨ fung vorgestellten symbolischen Bildberechnungen proﬁtieren von kompakteren u IMDs und k¨ nnen mit weniger Aufwand berechnet werden. Ein IMD wird mit fol- o genden Regeln reduziert: 1. Wenn ein Nichtterminalknoten v ∈ VN nur eine ausgehende Kante mit der neu- tralen Abbildungsfunktion in einen Knoten v besitzt, kann v entfernt werden, und alle vorher in v eingehende Kanten zeigen auf v . 2. Wenn unterschiedliche Nichtterminalknoten mit gleichem Index und gleicher Menge von Abbildungsfunktionen existieren, und diese jeweils die gleichen Nachfolger haben, werden all diese Knoten bis auf einen entfernt, und deren ¨ eingehende Kanten zeigen auf den ubrigen Knoten. 3. Wenn ein Nichtterminalknoten v ∈ VN Kanten mit gleicher Abbildungsfunktion hat, werden diese durch eine Kante mit dieser Abbildungsfunktion zu einem neu- en Knoten w mit Index gleich dem h¨ chsten Index der Nachfolger von v ersetzt. o Haben alle Nachfolger von v den gleichen Index, bekommt der neue Knoten w all deren ausgehende Kanten, und alle Nachfolger von v werden bis auf den neu erstellten Knoten w entfernt. Haben die Nachfolger von v verschiedene Indices, bekommt der neue Knoten w alle ausgehenden Kanten der Nachfolger mit glei- chem Index, die entfernt werden. Eine Kante mit neutraler Abbildungsfunktion ¨ wird von dem Knoten w zu jedem ubrigen Nachfolgerknoten eingef¨ gt.u Anhand eines Beispiels aus [191] wird die symbolische Repr¨ sentation von Syste- a MoC-Modellen vorgestellt. Beispiel 8.1.5. Gegeben ist das SysteMoC-Modell aus Abb. 2.13 auf Seite 70. Die symbolische Repr¨ sentation des Anfangszustands als IDD ist in Abb. 8.7a) zu sehen. a Im Anfangszustand des Modells sind alle Kan¨ le bis auf c6 leer. Kanal c6 enth¨ lt a a ¨ anfangs eine Marke. In der Darstellung wurden zur Ubersichtlichkeit alle Kanten zu dem Terminalknoten mit Wert F entfernt. Der abstrakte Zustand eines Modells, wie in Abschnitt 8.1.1 beschrieben, l¨ sst sich wie folgt als IDD codieren: a • F¨ r jeden FIFO-Kanal ci wird eine Variable ci # mit Deﬁnitionsbereich [0, ni ] u ben¨ tigt, wobei ni der Tiefe des FIFO-Kanals ci , entspricht. In diesem Beispiel o wird davon ausgegangen, dass die FIFO-Kan¨ le eine beschr¨ nkte Gr¨ ße von 8 a a o besitzen. Somit ist der Deﬁnitionsbereich ∀1 ≤ i ≤ 6 : ci # ∈ [0, 8]. • F¨ r jeden Aktor mit mehr als einem Zustand wird eine Variable mit dem Deﬁ- u nitionsbereich [0, si − 1] ben¨ tigt, wobei si gleich der Anzahl der Zust¨ nde des o a Aktors ist. In dem Beispiel aus Abb. 2.13 besitzt lediglich der Aktor SqrLoop mehr als einen Zustand, weshalb q1 ∈ [0, 1] gilt, wobei q1 = 0 f¨ r den Zustand u start und q1 = 1 f¨ r den Zustand loop steht. u Abbildung 8.7b) zeigt die Erreichbarkeitsmenge des SysteMoC-Modells Abbil- dung 8.7c) zeigt ein IMD, welches die drei Transitionen des Aktors SqrLoop dar- stellt. Darin entspricht jeder der drei Pfade von dem Quellknoten zu dem Terminal- knoten einer der Transitionen. Im Unterschied zu IDDs sind an den Kanten zwei ¨ Intervalle und eine Funktion annotiert, die der Anderung einer Variablen durch die Transition entsprechen.