Digitale Hardware/ Software-Systeme - Part 21

Digitale Hardware/ Software-Systeme- P21:Getrieben durch neue Technologien und Anwendungen wird der Entwurf eingebetteterSysteme zunehmend komplexer. Dabei ist eine Umsetzung als Hardware/Software-System heutzutage der Stand der Technik. Die Minimierung von Fehlern imEntwurf dieser Systeme ist aufgrund deren Komplexit¨at eine der zentralen Herausforderungenunserer heutigen Zeit. Bereits heute wird mehr Aufwand in die Verifikation,also in die U¨ berpru¨fung der Korrektheit, eines eingebetteten Systems gestecktals in den eigentlichen Entwurf....
Nội dung trích xuất từ tài liệu:
Digitale Hardware/ Software-Systeme - Part 21594 Sachverzeichnis relatives Komplement, 523 konstantes, 276Mikroarchitektur 291 lineares, 276 mit Ausnahmebehandlung, 293, 311–312 Momentengraph mit dynamischer Instruktionsablaufpla- bin¨ rer, siehe BMD a nung, 293, 313–322 Monitor 103, 107, 189, 323 mit Fließbandverarbeitung, 293–308 Monitorschaltung 323 mit Multizyklen-Funktionseinheit, 293, MPSoC 2 308–311 MTBDD 275 mit Sprungvorhersage, 293, 312–313 Multi-Processor System-on-Chip 2 superskalare, 293 Multigraph 530Miter 246MoC 16 NachbedingungModallogik 24 st¨ rkste, 431 amodel of computation siehe MoC Nebenl¨ ufigkeit 43 aModell Netzwerk 531 heterogenes, 56 Boolesches, 525Modellpr¨ fer u Interpretation 526 CBMC, 449 Netzwerkkalk¨ l 508 u CMC, 449 NFA 47 F-Soft, 450 Definition, 47 Java Pathfinder, 449 Normalform, konjunktive 247, 543 SATABS, 449 ¨ Null-Aquivalenzproblem 129 SLAM, 449 SPIN, 449 OBDD 535 VeriSoft, 449 reduziertes, siehe ROBDD ZING, 449 OBMD 277Modellpr¨ fung 26, 106, 156, 178–207 u reduzierter, siehe ROBMD Abstraktionsverfeinerung OFDD 538 von Programmen 425 reduziertes, siehe ROFDD BDD-basierte, 156 Off-Testfall 137 CTL, 179–185 OIDD 460 existentielle, 200 reduziert, siehe ROIDD explizite, 106, 156, 178–188 OKFDD 539 implizite, 106, 185 reduziertes, siehe ROKFDD LTL, 185–188 On-Testfall 137 SAT-basierte, 156 open fault 6 von Hardware 331–345 Operandenbereich 382 von Programmen 422–425 Operator SE-LTL, 473–474 modellogischer, siehe Pfadquantor simulative, 27 temporaler, 73, 76 symbolische, 106, 156, 197–207 Finally 76 BDD-basierte 197–199 Globally 76 SAT-basierte 199–207 Next 76 TCTL, 211–222 Release 76 TLM, 476–484 Until 76 universelle, 200 von Programmen, 422–431 p-use 410, 412Modulebene 14, 15 Pareto-Optimum 9, 18Moment Partialordnung 524 Sachverzeichnis 595Partialordnungsreduktion 158, 172–178 Modellpr¨ fung 211–214 uPartition Pr¨ fung des Zeitverhaltens 207–214 u einer Menge, 523 Zustandsklassen 208Partitionsblock 523 Zustandsgleichung, 168path segment simulation 436 PEUF 357Periode 349 PfadPetri-Netz 41, 91 definitionsfreier, 412 Anfangsmarkierung, 41 kritischer, 346 Beschr¨ nktheit, 44, 164 a l¨ ngster, 346 a Definition, 41 Pr¨ fix, 74 a Dynamisierungsvorschrift, 41 Suffix, 74 Erreichbarkeitsmenge, 44 Pfadberechnung 135 Flussrelation, 41 Pfadberechnungsanpassung 138 Folgemarkierung, 43 Pfadbereich 135 Grundzustand, 157, 165, 167 Pfadbereichsanpassung 138 Inzidenzmatrix eines, 168 Pfadbereichstest 134–139 Kanten, 41 Pfaderg¨ nzung 138 a Kantengewichte, 41 Pfadgewicht 531 Konflikt, 43 Pfadquantor 78 Konservativit¨ t, 45, 170 a existentieller, 78 Lebendigkeit, 44 universeller, 78 Marke, 42 Plattformmodell 17 Markierung, 42 point to analysis 449 Markierungsfunktion, 42 Polynom 117 Nachbereich eines Knotens, 42 sparse recursive representation, 118 Netzgraph, 41 verschwindendes, 291 Reversibilit¨ t, 45, 156, 165, 167, 171 a Polynomfunktion 119 Schaltregel, 43 polynomieller Algorithmus 542 schwache Lebendigkeit, 44 Potenzmenge 523 Sicherheit, 44, 156 Pr¨ dikatenabstraktion 426 a starke Lebendigkeit, 44, 167 Pr¨ dikatenintervall 462 a Stelle, 41 Pr¨ dikatenlogik 528 a Kapazit¨ t einer 41 ...