Formale Analyse von Sequential Function Charts

点击翻译按钮获取中文摘要

Ziel des Projektes ist die Bereitstellung eines Rechnerwerkzeugs zur formalen Analyse von Softwarespezifikationen auf der Basis von Sequential Function Charts. Da in Vorarbeiten der Antragsteller bereits eine entsprechende Werkzeugunterstützung für die Spezifikationssprache Statecharts (SCs) realisiert wurde und die beiden Spezifikationsmittel im wesentlichen auf einer gemeinsamen Modellgrundlage beruhen, soll dieses Ziel durch eine Einbindung der SFCs in diesen Ansatz erreicht werden. Konkret bedeutet das, daß die gleiche Zwischendarstellung verwendet wird, die in den Vorarbeiten schon als Schnittstelle zwischen SCs und den Modelcheckern diente, nämlich Hierarchische Automaten (HAen). Den Kern des Projektes bildet daher die Entwicklung eines Transformationsverfahrens, das SFCs in HAen abbildet und so die Anwendung der für dieses Spezifikationsmittel bereits zur Verfügung stehenden Werkzeuge ermöglicht. Dies soll zunächst für SFCs und HAen ohne Zeitbehaftung geschehen und in einem zweiten Schritt auch Echtzeitspezifikationen erweitert werden.