Digitale Hardware/ Software-Systeme- P27: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. | 514 8 Systemverifikation sehen. Die runden Knoten bezeichnen dabei Quellen bzw. Senken von Ankunftsund Servicekennlinien d. h. sie modellieren die Umgebung des Systems. So wird beispielsweise die Ankunftsrate von Paketen beschrankt. Die Rechtecke bezeichnen die Transformation der Ankunfts- und Servicekennlinien entsprechend Abb. . Man beachte dass im Echtzeitkalkül Kommunikation genauso wie Berechnungen auf Prozessoren behandelt wird. Abb. . Zeitbewertungsnetzwerk für den Netzwerkprozessor aus Abb. 429 Modulare Zeitanalyse zyklischer markierter Graphen In Abschnitt 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. auf Seite 356 . Da Implementierungen mit beschranktem Speicher auskommen müssen wurden FIFO-Kanale mit beschrankter Kapazität durch zusätzliche rückwärts gerichtete Kanten Zeitanalyse auf Systemebene 515 mit Anfangsmarkierung modelliert. Dadurch wurden Ressourcenbeschrankungen für die Kanäle berücksichtigt. Ressourcenbeschrankungen für die Aktoren wurden durch Selbstschleifen mit einer einzelnen Anfangsmarke modelliert wodurch ein Aktor stets erst nach Beendigung einer Berechnung die nachste Berechnung starten kann. Aktoren sind in diesem Modell dediziert gebunden d. h. jeder Aktor entspricht einer Hardware-Komponente. In diesem Abschnitt wird beschrieben wie die modulare Zeitanalyse für Systeme bei denen mehrere Aktoren auf die selben HardwareKomponente gebunden sein können angewendet werden kann. Modellierung markierter Graphen Gegeben sei ein markierter Graph G A C M0 mit Aktoren a e A Kanalen c e C Q A x A und der Anfangsmarkierung M0 C R 0. Man beachte dass die Markierung eines Kanals kontinuierlich sein kann. Dies schließt selbstverstandlich den Fall ein dass Marken diskret sein konnen. Ein Aktor verarbeitet einen Strom aus Marken der als Ereignisstrom modelliert wird. Die Anzahl zu
