Hohe Entwicklungskosten und lange Entwicklungszeiten beeinträchtigen die Wettbewerbsfähigkeit eines signaltechnische Bahnreinrichtungen entwickelnden Unternehmens. Die Forderungen nach Neustrukturierung und effizienterer Gestaltung der Entwicklungsprozesse werden durch neue europäische Normen verschärft. Zu den aus der Sicht der System- und Software-Entwicklung wichtigen normativen Neuerungen gehört die Forderung nach dem Einsatz formaler Beschreibungsmittel und formaler Methoden. Im Rahmen des Arbeitskreises FORMS wurde ein Anforderungskatalog für formale Beschreibungsmittel entwickelt, der eine Auswahl unterstützen und erleichtern soll. Eine Voraussetzung zur Erfüllung der Anforderungen der CENELEC-Normen ist die Definition, Erprobung und die stufenweise Einführung eines modellbasierten werkzeuggestützten Entwicklungsprozesses. Das Ziel des vorliegenden Beitrags ist die Vorstellung ausgewählter Beschreibungsmittel und Verfahren anhand der eingesetzten Werkzeuge. In diesem Kontext werden die Themen 'Requirement Engineering', 'Requirement Tracing', Erstellung sowie Verifikation formaler Modelle behandelt. Besondere Aufmerksamkeit wird der formalen Verifikation der Modelle gewidmet. Das Werkzeug 'Statemate' stellt eine integrierte Umgebung zur Analyse, zum Entwurf und zur Dokumentation von formalen Modellen für technische Systeme (insbesondere für eingebettete Systeme) zur Verfügung. Zentrales Konzept ist hier, daß Benutzern ein visueller Formalismus zur Verfügung gestellt wird. Dies erhöht in vielen Anwendungsgebieten die Übersichtlichkeit, steigert das intuitive Verständnis und erleichtert die Kommunikation zwischen den Entwicklern. Statemate mit seinen Sprachen Acitivity-Charts und Statecharts wird vornehmlich in frühen Stufen eines modellbasierten Entwicklungsprozesses eingesetzt und unterstützt die Spezifikation von Systemen auf hoher Abstraktionsebene. Beispielhaft wird die Vorgehensweise anhand der Fallstudien 'funkbasierter Bahnübergang' und 'Hp-Schnittstelle' aufgezeigt. Die Arbeit an den Fallstudien hat gezeigt, daß insbesondere der zielgerichtete Einsatz formaler Verifikation zum Nachweis von Anforderungen sich als sehr nützlich zur Fehlerentdeckung und zur Fehlersuche erwiesen hat.
Modellierung der Forms-Fallstudien mit Statemate
2000
48 Seiten, 29 Bilder, 2 Tabellen, 14 Quellen
Conference paper
German
Statemate basierte Modellierung und Verifikation von Steuerungssystemen: Konzepte und Anwendung
British Library Conference Proceedings | 2000
|Department highlights - METEOR guided by Statemate
Online Contents | 2005
Formale Analyse und Verifikation von Statemate-Entwürfen
IuD Bahn | 2001
|I-Logix launches new version of Statemate MAGNUM
Emerald Group Publishing | 2001