Informationen zum Teamprojekt in Theoretischer Informatik und Software Engineering
Academic partner of Esterel Technologies, the provider of model-based solutions for
DO-178B and IEC 61508 safety-critical systems.
Academic partner of Esterel EDA Technologies
provider of ESL synthesis
for control-intensive IP design and verification,
including SystemC,
VHDL, and Verilog code generation
Material zum Herunterladen
- NEU Beispiel der Laufzeitumgebung von Axel Zechner
- Aktuelle Version der ZLB-Software (inkl. C++ Betriebslogik)
- Folien des Kickoff-Meetings
- Text zu Grundlagen der ZLB-Logik
- Axel Zechners Diplomarbeit über die Architektur eines ZLB Protection Systems
- Johannes Kloos' Diplomarbeit zur Erstellung einer Testumgebung für das ZLB-PS
- Unfertige Verhaltensspezifikation von ZLB-PS (war Ausgangspunkt für letzten Punkt)
- C++ Implementierung der Betriebslogik
- Testumgebung von Johannes
Kloos für die Betriebslogik. Zum Übersetzen braucht man folgende
Werkzeuge und Bibliotheken:
1. cmake zur Erstellung des Makefiles bzw. des Visual Studio-Projekts (siehe http://www.cmake.org)
2. die boost-Bibliothek (siehe http://www.boost.org/)
3. die Bibliotheken xalan-c und xerces-c (siehe http://xml.apache.org/). Zum Übersetzen: Zuerst erzeugt man mittels cmake (Aufruf: "cmake .") ein Makefile bzw. VS-Projekt, das man dann anschließend übersetzt. Dabei sollte ein einzelnes Programm herausfallen (testharness.exe).
Momentan erwartet der testharness, dass ZLB-PS auf localhost, Port 22222 läuft (kann bei Bedarf gerne geändert werden).
- Schulungsunterlagen und Themenübersicht der Blockveranstalung zu SCADE im Rahmen der Vorlesung "Sicherheitsrelevante Softwaresysteme"
Allgemeine Informationen
Ziel des Projektes ist die Anwendung der SCADE Certified Software Factory, einer Tool-Suite für die modellbasierte Softwareentwicklung, auf ein Forschungsbeispiel aus der Eisenbahnautomatisierung, das sich aus einer Zusammenarbeit mit der Siemens AG in Braunschweig ergibt.
SCADE ist eine Modellierungsprache für die Software eingebetteter Systeme. Der SCADE-Semantik liegt die synchrone Hypothese zugrunde: SCADE-Modelle sind zyklisch synchron getaktete Datenfluss- und Zustandsmaschinen (siehe Abbildung 1). Aus den Modellen wird mittels eines Code-Generators C-Code generiert.
Im Projekt soll eine vereinfachte logische Steuerung für die technische Automatisierung der Betriebsabläufe (hier Betriebslogik genannt) im Zugleitbetrieb für das System ZLB-PS (Zugleitbetrieb Protection System) in SCADE modelliert und in einen vorhandenen Prototypen integriert werden. Zugleitbetrieb (ZLB) ist ein Verfahren zur Zugsicherung, das auf eingleisigen Strecken mit geringem Belastungsprofil zum Einsatz kommt und im Normalfall auch ohne technische Unterstützung auskommt. Das Betriebslogik-Modell soll eine konfigurierbare Komponentenarchitektur aufweisen. Die Betriebslogik soll die Abhängigkeiten auf Basis des in der Stellwerksentwicklung etablierten Spurplanprinzips verarbeiten. Das bedeutet, dass einzelne Komponenten (Weichen, Signale, Gleiselemente etc.) mit einfacher fester Funktionalität flexibel zu beliebigen Stellwerken kombiniert werden können. Als Beispiel soll das in Abbildung 2 gezeigte Beispielgleisbild umgesetzt werden. Insgesamt ist zu beachten, das die Umgebung der zu modellierenden Komponente (wie die Realität) asynchron aufgebaut ist.
Teilaufgaben:
- Beschreibung der Architektur der Betriebslogikkomponente
- Erstellung von SCADE-Modellen für Stellteile (Weiche, Signale etc.), die die logische Ansteuerung einzelner Außenelemente implementieren
- Erstellung eines SCADE-Modells, das die übergeordnete Steuerungs-Logik umsetzt
- Aufbau einer Kommunikationsstruktur zwischen den einzelnen Elementen und der zentralen Steuerungslogik
- Umsetzung von Beispielen (wie obiges Gleisbild) mit den erstellten Komponenten
- Integration dieser Beispiele in ein vorhandenes Testbett; dazu muss in C ein Wrapper zur Anbindung des Modells an das Testbett implementiert werden
- Test der Betriebslogik mit vorhandenen Testfällen
- Optional (abhängig vom Vorhandensein in der SCADE-Toolsuite): formale Verifikation des Modells mit dem SCADE Design-Verifier