Bitte wählen Sie ihr Lieferland und ihre Kundengruppe
In diesem Artikel stellen die Autoren eine Form von zeitannotierten synchronen Kommunikationsnetzwerken als Abstraktion von synchron kommunizierenden Automaten auf der Basis von Kripke-Strukturen vor. Diese Kommunikationsnetzwerke stellen im Prinzip eine synchrone Variante der Kahn Prozess-Netzwerke (KPNs) dar. Unsere synchronen Kommunikationsnetzwerke bestehen aus endlichen Automaten, die über gerichtete Ports mit endlichen FIFO-Kommunikationspuffem verbunden sind und durch den Austausch typisierter Datenobjekte miteinander kommunizieren. Zur direkten semantikerhaltenden Abbildung auf Kripke-Strukturen ist die Ausführung der endlichen Automaten über einen globalen Taktgeber synchronisiert, so dass das globale Berechnungsmodell zur synchronen Kommunikation in zwei globale Phasen unterteilt ist: (i) Lokale Berechnung und (ii) Kommunikationsphase. Auf Basis dieser Netzwerke wird eine Heuristik zur statischen Berechnung und Generierung von laufzeiteffizientem Code für den RAVEN Model-Checker vorgestellt und anhand eines Fallbeispiels näher erläutert.