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.

Cite

Citation style:

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

Access Statistic

Total:
Downloads:
Abtractviews:
Last 12 Month:
Downloads:
Abtractviews:

show details

Rights

Use and reproduction:
All rights reserved

Export