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

Rumpe, Bernhard GND; Gajanovic, Borislav

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.

Vorschau

Zitieren

Zitierform:

Rumpe, Bernhard / Gajanovic, Borislav: Isabelle/HOL-Umsetzung strombasierter Definitionen zur Verifikation von verteilten, asynchron kommunizierenden Systemen. Braunschweig 2006. Institut für Software Systems Engineering.

Zugriffsstatistik

Gesamt:
Volltextzugriffe:
Metadatenansicht:
12 Monate:
Volltextzugriffe:
Metadatenansicht:

Details anzeigen

Rechte

Nutzung und Vervielfältigung:
Alle Rechte vorbehalten

Export