×

zbMATH — the first resource for mathematics

Specification and verification of polling real-time systems. (English) Zbl 0953.68087
Oldenburg: Univ. Oldenburg, Fachbereich Informatik, xvi, 227 p. (1999).
Zusammenfassung: Die Korrektheit von Realzeitsystemen ist ein wichtiger Gegenstand der aktuellen Forschung im Bereich der Formalen Methoden. Ziel ist es, die zusätzliche Problematik “Zeit” bei der Spezifikation und Verifikation in den Griff zu bekommen. In dieser Arbeit wird ein Ansatz vorgestellt, korrekte Realzeitprogramme für Speicherprogrammierbare Steuerungen (SPSen) zu entwickeln. Diese Hardware arbeitet zyklisch wiederkehrend ein Programm ab, wobei die Dauer für einen Zyklus nach oben beschränkt ist. Dieses zyklische Verhalten ist eine sehr häufig anzutreffende Variante, Kontrollprogramme für Steuerungen zu entwickeln, die auch auf anderen Hardwareplattformen implementiert werden, so daß sich die hier vorgestellte Methode auch auf solche Steuerungen erweitern läßt. Motiviert sind die Arbeiten durch das BMBF-Projekt UniForM (Universelle Entwicklungsumgebung für Formale Methoden), das unter anderem auf die Verifikation von SPS-Programmen abzielte.
Zentral für unseren Ansatz ist das Konzept des “SPS-Automaten”, der eine abstrakte Sicht auf Speicherprogrammierbare Steuerungen darstellt. Für SPS-Automaten werden folgende Ergebnisse präsentiert:
SPS-Automaten lassen sich in Programmiersprachen für SPSen compilieren. Außerdem werden Anforderungen an die Geschwindigkeit der SPS und an die Genauigkeit der Zeitmessung generiert. Es wird eine logische Semantik erarbeitet, die durch Formeln des Duration Calculus (DC), einer Intervall-basierten temporalen Logik, dargestellt wird. Dadurch kann man leichter zeigen, daß ein SPS-Automat Anforderungen erfüllt, die in dem UniForM-Ansatz ebenfalls im DC spezifiziert werden. Da die DC-Semantik das zyklische Verhalten, die Rechengeschwindigkeit und die Zeitmessungstoleranzen berücksichtigt, wird eine realistische Beschreibung der Wirklichkeit gegeben. Verschiedene Kompositionsmöglichkeiten von SPS-Automaten werden definiert und semantisch beschrieben. Dabei orientieren sich die Definitionen der Kompositionsoperatoren an den Möglichkeiten, die für SPSen natürlich erscheinen. Zusätzlich gibt es eine operationelle Semantik, die durch “Timed Automata” beschrieben wird und die beweisbar konsistent zu der DC-Semantik ist. Durch die Existenz dieser Semantik ist es möglich, bereits vorhandene Model-Checker für Timed Automata als Model-Checker für SPS-Automaten zu nutzen. Weiterhin werden Abstraktionstechniken vorgestellt, die aus SPS-Automaten entstehenden Timed Automata Modelle verkleinern und so das Model-Checking effizienter machen können. Für die sogenannten DC-Implementables, eine Subsprache des Duration Calculus, gibt es ein Verfahren, das aus einer beliebigen Spezifikation bestehend aus diesen Implementables einen SPS-Automaten formal synthetisiert, der die Spezifikation erfüllt, sofern ein solcher überhaupt existiert. Abschließend werden einige Fallbeispiele, die von akademischer als auch industrieller Natur sind, mit SPS-Automaten bearbeitet, wobei ein Werkzeug für SPS-Automaten zum Einsatz kommt.
Zusammenfassend stellen SPS-Automaten ein formales Modell dar, daß auf eine weitreichende Klasse von Realzeitkontrollprogrammen anwendbar ist und für diese Klasse automatische Methoden zur Verifikation anbietet.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68-02 Research exposition (monographs, survey articles) pertaining to computer science
Keywords:
SPS Automaton
Software:
SIGNAL
PDF BibTeX XML Cite