Isabelle/HOL-Umsetzung strombasierter Definitionen zur Verifikation von verteilten, asynchron kommunizierenden Systemen

Dieser technische Bericht beschreibt grundlegende Datenstrukturen, Funktionen und Prin-zipien zur Verifikation des Verhaltens verteilter, asynchron kommunizierender Systeme wie etwa Bussysteme im Auto, Telekommunikationsnetzen oder dem Internet. Dazu werden die im Focus-Ansatz [BS01] eingeführten Ströme im Theorembeweiser Isabelle [NPW02] in komfortabler Weise so umgesetzt, dass sowohl verteilte Komponenten als auch Protokolle zwischen Komponenten einfach und elegant definiert und ihre Eigenschaften untersucht werden können. Zur Verfügung stehen Techniken zur Definition von Liveness-und Fairness-Eigenschaften, schnittstellenbasierte Komposition und Verfeinerungstechniken, die miteinander kompatibel sind. Die Focus-Theorie basiert im Wesentlichen auf der Formalisierung von Kommunikationshistorien und von Komponenten als mathematische Funktion, die Eingabe- und Ausgabehistorien abbildet. Das hier vorgestellte Modell für potentiell unendliche Ströme nutzt einen grundlegenden neuen Datentypkonstruktor fstream, der zwar auf HOLCF beruht, in dessen Umgang aber der Anwender nicht explizit auf HOLCF angewiesen ist. Dadurch ist HOLCF vor dem Anwender verborgen.