Ein Kalkül zur Spezifikation, Entwurf und Verifikation verteilter paralleler Systeme

Ein Kalkül zur Spezifikation und Verifikation verteilter paralleler interaktiver Echtzeitsysteme wird vorgestellt. Systeme werden durch ihr Schnittstellenverhalten spezifiziert, das durch Schnittstellenvorbedingungen und Schnittstellenaussagen formalisiert ist. Systementwürfe in Bezug auf Architekturen verteilter Netzwerke interaktiver Systeme werden durch parallele Zusammensetzung von Teilsystemen konstruiert. Die Spezifikation von Systementwürfen wird aus den Spezifikationen ihrer Teilsysteme berechnet. Die Verifikation erfolgt durch Beweisregeln, die auf den Konzepten von Kausalität und Realisierbarkeit basieren und durch das operationale Modell in Form von verallgemeinerten Moore-Maschinen, die nicht auf endliche Zustandsräume beschränkt sind, gerechtfertigt sind. Das Kalkül unterstützt die Schnittstellenspezifikation und Überlegungen sowohl über unzeitliche als auch über zeitgesteuerte verteilte parallele Systeme. Dies umfasst den Entwurf von cyber-physischen Systemen. Echtzeit wird insbesondere verwendet, um zeitkritisches Verhalten zu spezifizieren und Eigenschaften zu beweisen, die mit Kausalität und Realisierbarkeit zusammenhängen, Eigenschaften, die für alle Moore-Maschinen gelten. Auf dieser Grundlage wird ein Kalkül ausgearbeitet und anhand kleiner Beispiele veranschaulicht. Der Kalkül wird als konsistent und relativ vollständig nachgewiesen.