Digitale Hardware/ Software-Systeme- P21: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 | 594 Sachverzeichnis relatives Komplement 523 Mikroarchitektur 291 mit Ausnahmebehandlung 293 311-312 mit dynamischer Instruktionsablaufpla- nung 293 313-322 mit Fließbandverarbeitung 293-308 mit Multizyklen-Funktionseinheit 293 308-311 mit Sprungvorhersage 293 312-313 superskalare 293 Miter 246 MoC 16 Modallogik 24 model of computation siehe MoC Modell heterogenes 56 Modellprüfer CBMC 449 CMC 449 F-Soft 450 Java Pathfinder 449 SATABS 449 SLAM 449 SPIN 449 VeriSoft 449 ZING 449 Modellprüfung 26 106 156 178-207 Abstraktionsverfeinerung von Programmen 425 BDD-basierte 156 CTL 179-185 existentielle 200 explizite 106 156 178-188 implizite 106 185 LTL 185-188 SAT-basierte 156 von Hardware 331-345 von Programmen 422-425 SE-LTL 473-474 simulative 27 symbolische 106 156 197-207 BDD-basierte 197-199 SAT-basierte 199-207 TCTL 211-222 TLM 476-484 universelle 200 von Programmen 422-431 Modulebene 14 15 Moment konstantes 276 lineares 276 Momentengraph binarer siehe BMD Monitor 103 107 189 323 Monitorschaltung 323 MPSoC 2 MTBDD 275 Multi-Processor System-on-Chip 2 Multigraph 530 Nachbedingung stärkste 431 Nebenlaufigkeit 43 Netzwerk 531 Boolesches 525 Interpretation 526 Netzwerkkalkul 508 NFA 47 Definition 47 Normalform konjunktive 247 543 Null-Aquivalenzproblem 129 OBDD 535 reduziertes siehe ROBDD OBMD 277 reduzierter siehe ROBMD OFDD 538 reduziertes siehe ROFDD Off-Testfall 137 OIDD 460 reduziert siehe ROIDD OKFDD 539 reduziertes siehe ROKFDD On-Testfall 137 openfault 6 Operandenbereich 382 Operator modellogischer siehe Pfadquantor temporaler 73 76 Finally 76 Globally 76 Next 76 Release 76 Until 76 p-use 410 412 Pareto-Optimum 9 18 Partialordnung 524 Sachverzeichnis 595 Partialordnungsreduktion 158 172-178 Partition einer Menge 523 Partitionsblock 523 path segment Simulation 436 Periode 349 Petri-Netz 41 91 Anfangsmarkierung 41 Beschränktheit 44 164 Definition 41 Dynamisierungsvorschrift 41 Erreichbarkeitsmenge 44 Flussrelation 41 Folgemarkierung 43 Grundzustand 157 165 167 .
