MySZ. Ein Ansatz zur systematischen Verbindung von Z und Statecharts

In diesem Report beschreiben wir den Spezifikationsformalismus My-SZ, der als Grundlage für die Integration von Statecharts und Z im ESPRESS Projekt dienen soll. My-SZ stellt einen hybriden Formalismus zur Spezifikation von Prozessen zu Verfügung: dynamisches Prozeßverhalten wird durch zeitbehaftetete Statecharts und das Datenmodell durch Z beschrieben. My-SZ umfasst einen Komponentenbegriff, der die Beschreibung von Prozeßobjekten durch Prozeßklassen in modularer Weise unterstützt. Aggregation und Assoziation von Prozeßobjekten wird über sogenannte Konfigurationen ermöglicht, die die (statische) Instantiierung von Prozeßklassen und die Definition von Sichtbarkeitsbereichen von Broadcastnachrichten realisieren. Generizität und Umbenennung bzw. Parametrisierung unterstützen die Formulierbarkeit von Kommunikationsbausteinen, die auf der Grundlage von Broadcasting High-Level Konzepte wie entfernte Operationsaufrufe und synchrone Kanalkommunikation implementieren.