scientific article; zbMATH DE number 1258216

Diese Arbeit beschäftigt sich mit dem formalen architekturbezogenen Entwurf verteilter Systeme. Ziel der Arbeit ist die Unterstützung des hierarchischen Entwurfs durch eine Integration prozeßalgebraischer und temporallogischer Spezifikations- und Verifikationstechniken. Die betrachteten Systeme bestehen aus einer gegebenen Anzahl von sequentiell arbeitenden Komponenten, die über gemeinsame Aktionen kommunizieren. Durch die Verteilung der Systemaktionen auf die Komponenten ist die Kommunikationsstruktur und damit die Architektur festgelegt. Als Formalisierung eines Implementierungsschrittes im hierarchischen Entwurf wird die prozeßalgebraische Methode der Aktionsverfeinerung betrachtet. Wir definieren eine lokalitätsbasierte Prozeßalgebra zur Spezifikation derartiger Systeme und entwickeln eine operationelle Semantik, die auch als eine kausalitätsbasierte Semantik verstanden werden kann. Durch Aktionsverfeinerung kann die Implementierung einer Aktivität, die auf einer abstrakten Spezifikationsebene als eine Aktion betrachtet wurde, durch einen komplexen verteilten Prozeß beschrieben werden. Die Vorgabe der Systemarchitektur erlaubt es, für jede Komponente eine eigene lokale Implementierung einer abstrakten Aktion, an der mehrere Komponenten teilnehmen, anzugeben. Auf der Ebene einzelner Komponenten betrachtet entspricht dieser neue Verfeinerungsbegriff dem Konzept des Prozeduraufrufs in sequentiellen Systemen. Dadurch ist zwar die Implementierbarkeit innerhalb der vorgegebenen Architektur garantiert, allerdings können im allgemeinen ohne Analyse der Einzelkomponenten kaum Aussagen über das Verhalten des Gesamtsystems nach einem Verfeinerungsschritt gemacht werden. Wir untersuchen daher Bedingungen an die Implementierungen einzelner Aktionen, die auch auf der Ebene der Systeme die Verwendung kompositioneller Beweistechniken aus der Theorie der Prozeßalgebren für diesen Aktionsverfeinerungsbegriff ermöglichen. Zusätzlich zeigen wir, wie restriktivere, aus der Literatur bekannte Verfeinerungsbegriffe mit Hilfe kanonischer Verfeinerungen in unseren Ansatz integriert werden können. Des weiteren wird die Vererbung von temporallogischen Anforderungsspezifikationen unter Aktionsverfeinerung untersucht. Das Ziel ist es, die Verifikation von Verhaltenseigenschaften auf der Implementierungsebene zu vermeiden oder wenigstens zu erleichtern, indem eine entsprechende Eigenschaft bereits auf der abstrakten Spezifikationsebene nachgewiesen wird. Wir diskutieren die Anforderungen, die eine temporale Logik erfüllen muß, um mit dem architekturbezogenen Ansatz einerseits und Aktionsverfeinerung andererseits verträglich zu sein. Eine geeignete Logik ist \(\nu\)TrPTL, eine lokalitätsbasierte Linear-Time-Logik, deren einzige temporale Operatoren Next-Modalitäten sind, die über dem Aktionsalphabet und den Komponenten parametrisiert sind. Die Ausdrucksstärke der Logik wird über Fixpunktoperatoren erreicht. Wir definieren drei Transformationen auf Teillogiken von \(\nu\)TrPTL. Sie überführen temporallogische Formeln von der abstrakten Beschreibungsebene in Formeln für die Implementierungsebene auf Grundlage der prozeßalgebraischen Beschreibung der Verfeinerung von Aktionen. Wir zeigen, daß unter geeigneten Einschränkungen der Verfeinerungsfunktion eine temporallogische Formel genau dann für ein System gilt, wenn die transformierte Formel auf der Implementierungsebene erfüllt ist. Die Prozeßalgebra enthält einen speziellen Operator zur Spezifikation von rekursivem Verhalten, für das Terminierung gewährleistet ist. Dieser Operator erlaubt es, derartiges endlich rekursives Verhalten in den Verfeinerungen der Aktionen zuzulassen und trotzdem die Vererbung von Lebendigkeitseigenschaften unter Verfeinerung nachzuweisen. Wir zeigen die Nützlichkeit dieses Operators anhand eines Beispiels, in dem eine Synchronisationsaktion mit Hilfe eines fehlerhaften Übertragungsmediums implementiert wird, das eine beliebige endliche Zahl von Nachrichten verlieren kann.

Recommendations

Cited in

(6)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4229096)