(MA) Komposition gewöhnlicher Differentialgleichungen mit sicherheitsrelevanten Zustandsautomaten

Betreuer: Frank Ortmeier,Simon Struck,Claudia Krull
Student: Sebastian Nielebock
Zeitraum: 30.4.2013 – 17.9.2013

 

Zusammenfassung:

Die Sicherheit technischer Systeme, wie Zugkontrollsysteme oder Atomkraftwerke, a-priori in der Modellphase zu zeigen, ist wünschenswert. Dabei ist eine gängige Möglichkeit, solche Systeme als diskrete Modelle zu abstrahieren und mittels diskreter Model Checker auf ihre Sicherheit hin zu prüfen. Besonderes Ziel ist es, sämtliche sicherheitsgefährdenden Situationen (engl. ,,hazard´´) zu finden. Obwohl einige Eigenschaften schon gezeigt werden können, sind diese Verfahren noch nicht für Systeme mit kontinuierlichem Verhalten geeignet. Dieses Verhalten kann typischerweise durch gewöhnliche Differentialgleichungen beschrieben werden.

Diesbezüglich wird in dieser Arbeit ein Algorithmus vorgestellt, der solche Gleichungen in diskrete Modelle integrieren kann. Konkret werden dabei Modelle in der Modellierungssprache SAML erzeugt. Mittels dieser transformierten Modelle können nun Hazards aus dem originalen Modell durch diskrete Model Checker gefunden werden. Dies wird mittels Beweisen gezeigt und anhand eines Beispiels demonstriert. Mittels experimenteller Analysen wird gezeigt, dass dieses Verfahren für kleinere Modelle mit einer Differntialgleichung effizient genutzt werden kann.

Abstract:

It is desirable to decide a-priori the safety of technical systems, like train control systems or nuclear power plants, during the modeling phase. A typical workflow is to abstract these systems as discrete models and to check their safety with discrete model checkers. A specific goal is to find all hazardous situations. Although many properties can be proved up to now, these approaches are not usable for systems with continuous behavior. Typically this behavior can be described by ordinary differential equations.

Therefore, this thesis presents an algorithm, which is able to integrate such equations into a discrete model. In particular, models of the modeling language SAML are created. With the help of these transformed models one is able to find hazards from the original model by discrete model checker. This is shown by proofs and is demonstrated with examples. By experimental analysis it is shown, that this approach is efficiently usable for small models with a single differential equation.

(MA) Komposition gewöhnlicher Differentialgleichungen mit sicherheitsrelevanten Zustandsautomaten