Please use this identifier to cite or link to this item: http://dx.doi.org/10.18419/opus-2602
Authors: Bitsch, Friedemann
Title: Verfahren zur Spezifikation funktionaler Sicherheitsanforderungen für Automatisierungssysteme in Temporallogik
Other Titles: Technique of specification of functional safety requirements for industrial automation systems in temporal logic
Issue Date: 2007
metadata.ubs.publikation.typ: Dissertation
Series/Report no.: IAS-Forschungsberichte;2007,1
URI: http://nbn-resolving.de/urn:nbn:de:bsz:93-opus-30415
http://elib.uni-stuttgart.de/handle/11682/2619
http://dx.doi.org/10.18419/opus-2602
ISBN: 978-3-8322-6035-4
Abstract: Durch formale Verifikation kann die Einhaltung funktionaler Sicherheitsanforderungen im Modell der Systemfunktionen eines Automatisierungssystems mit Sicherheitsverantwortung mit mathematischer Exaktheit überprüft werden. Eine Voraussetzung hierfür ist, dass die Sicherheitsanforderungen in einer formalen Spezifikationssprache, d. h. mit einer eindeutigen Syntax und Semantik, formuliert werden. Eine entscheidende Ursache für die wenig verbreitete Anwendung formaler Verifikation liegt in der Schwierigkeit der formalen Spezifikation temporaler Relationen, die bei der Formulierung funktionaler Sicherheitsanforderungen für Automatisierungssysteme ausgedrückt werden müssen. Wird die formale Spezifikationssprache nicht vollständig beherrscht, werden Sicherheitsanforderungen leicht fehlerhaft spezifiziert, woraus die Entwicklung eines Automatisierungssystems resultieren kann, von dem Gefahren ausgehen. Dasselbe ist der Fall, wenn eine Sicherheitsanforderung falsch interpretiert wird. Diesen Schwierigkeiten kann durch ein Verfahren begegnet werden, bei dem Expertenwissen für die formale Spezifikation von funktionalen Sicherheitsanforderungen vermittelt wird. Dies wird durch die Adaption und Nutzung von aus der Softwaretechnik bekannten Wiederverwendungskonzepten erreicht. Mithilfe des daraus resultierenden Safety-Pattern-Konzepts wird die Formalisierung funktionaler Sicherheitsanforderungen vereinfacht, indem Safety-Pattern mit generischen formalen Spezifikationen verwendet werden. Die Safety-Pattern, die für das jeweilige Spezifikationsproblem geeignet sind, müssen aus einem Katalog selektiert werden. Die korrekte Interpretation von Sicherheitsanforderungen, die mithilfe von Safety-Pattern spezifiziert worden sind, wird unterstützt, indem die Bedeutung im Safety-Pattern-Katalog nachgeschlagen werden kann. Um alle Arten funktionaler Sicherheitsanforderungen spezifizieren zu können, wurde der Katalog so entwickelt, dass er durch die Verwendung einzelner generischer Formulierungen sowie durch deren Komposition eine vollständige Grundlage zur Spezifikation aller Arten funktionaler Sicherheitsanforderungen für Automatisierungssysteme bietet. Darüber hinaus enthält der Katalog generische Formulierungen, durch welche die Handhabbarkeit des Verfahrens gewährleistet wird. Durch die Verwendung einer Safety-Pattern-Normsprache wird neben der formalen Spezifikation eine präzise und einfach interpretierbare Spezifikation funktionaler Sicherheitsanforderungen in einer eingeschränkten Terminologie der natürlichen Sprache ermöglicht. Zudem wurde eine spezielle grafische Notation für die Veranschaulichung komplizierter logischer Zusammenhänge entwickelt. Durch ein Werkzeugkonzept und den Einsatz multimedialer Techniken (Interaktionen, textuelle sowie grafische Beschreibungen und Simulationen) wird die Selektion, Interpretation und Instanziierung der Safety-Pattern unterstützt. Durch das Fallbeispiel „Eingleisiger Bahnübergang im Funk-Fahr-Betrieb“ wird die Anwendung des Verfahrens für die Entwicklung sicherer Automatisierungssysteme demonstriert.
For industrial automation systems with safety responsibility it is of vital importance to check the compliance of functional safety requirements. By means of formal verification it is possible to check with mathematical exactness if functional safety requirements are preserved in a model of the system functions. As a precondition, the safety requirements have to be specified in a formal specification language, i.e. that they are formulated with unambiguous syntax and semantics. It is highly challenging to specify formally temporal relations, which is compulsory for functional safety requirements of industrial automation systems. This is a decisive reason for the very rare use of formal verification. If the formal specification language is not mastered completely, then safety requirements will easily be falsely specified or will easily be misinterpreted. As a consequence unsafe industrial automation systems might be developed. Theses difficulties can be tackled by a technique, in which expertise on formal specification of functional safety requirements is imparted. This is achieved by adapting and utilizing reuse concepts, known from software engineering. The resulting safety patterns concept allows to simplify the formalisation of functional safety requirements as safety patterns with generic formal specifications are used. The safety patterns which are suitable for the respective specification problem have to be selected from a catalogue. The correct interpretation of safety requirements which have been specified on the basis of safety patterns is supported by the possibility to check their meaning in the safety patterns catalogue. The catalogue represents a complete basis for specifying all kinds of functional safety requirements for industrial automation systems by using single generic formulations as well as compositions of these formulations. Moreover, the catalogue contains generic formulations, which guarantee that the technique can be handled. Beside the formal specification, a safety patterns norm language allows to specify functional safety requirements in a precise and simply interpretable way by using a restricted terminology of natural language. In addition, a particular graphical notation has been developed in order to visualize complicated logical connections. The safety patterns selection, interpretation and instantiation are supported by a tool concept and by the use of multimedia technologies (interactions, textual as well as graphical descriptions and simulations). The appli¬cation of the safety patterns concept is demonstrated by means of the case study „single-track level crossing in radio-based operation“.
Appears in Collections:05 Fakultät Informatik, Elektrotechnik und Informationstechnik

Files in This Item:
File Description SizeFormat 
Dissertation_F_Bitsch.pdf2,47 MBAdobe PDFView/Open


Items in OPUS are protected by copyright, with all rights reserved, unless otherwise indicated.