Digitale Hardware/ Software-Systeme- P10: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. | 172 5 Eigenschaftsprüfung Beispiel . Für das Petri-Netz aus Abb. auf Seite 158 aus Beispiel folgt aus Gleichung -1 -1 0 0 1 i1 0 10 -10 0 i2 0 010 -10 . i3 0 1 0 0 1 -1 i4 0 0 1 1 0 -1 MV 0 Die kleinste ganzzahlige strikt positive Losung lautet iT 1 1 1 1 2 T. Die Existenz dieser Losung ist eine notwendige Bedingung für die Reversibilität des Petri-Netzes. Zu zeigen ist noch dass ein gültiger Ablaufplan beginnend mit der Anfangsmarkierung für den Schaltvektor existiert. Diese existiert allerdings nicht weshalb wie bereits zuvor mit den aufzahlenden Verfahren gezeigt das Petri-Netz irreversibel ist. Für alle anderen erreichbaren Markierungen kann allerdings mit der Stelleninvariante iT gezeigt werden dass es sich bei diesen Markierungen um Grundzustande des Petri-Netzes handelt. Partialordnungsreduktion Eine wesentliche Eigenschaft von Systemen mit nebenlaufigen Prozessen ist dass gültige Ausführungen dieser Prozesse in unterschiedlichen Reihenfolgen stattfinden können. Wahrend diese Eigenschaft im Entwurf zur Optimierung ausgenutzt werden kann stellt dies ein großes Problem bei der Verifikation solcher Systeme dar da hierdurch der zu untersuchende Zustandsraum sehr groß wird. Man spricht von der sog. Zustandsraumexplosion. Im Folgenden werden Moglichkeiten untersucht die es erlauben den Zustandsraum für Systeme mit nebenlaufigen Prozessen zu reduzieren. Oftmals hangt das Ergebnis der Verifikation von Systemen mit nebenlaufigen Prozessen gar nicht von der tatsächlichen Ausführungsreihenfolge ab. In einem solchen Fall ist es denkbar dass alle moglichen Permutationen in der Ausführungsreihenfolge durch eine einzelne ausgewahlte Ausführungsreihenfolge repräsentiert werden. Sei beispielsweise unter einer Markierung M die Ausführung der Folge t1 t2 moglich. Sei weiterhin unter M die Ausführung der Folge t2 t1 ebenfalls moglich und die beiden Schaltfolgen erreichen die selbe Folgemarkierung M d. h. M t1 t2 M M t2 t1 M so konnen die beiden .
