PUB - Publikationen an der Universität Bielefeld

The Ontological Hazard Analysis (OHA) is a specification and analysis method for system safety requirements, based on many small but rigorous refinement steps and causal analysis. This development sequence is applied to train-dispatching protocols as defined in the German railway standard FV-NE. Ontological Hazard Analysis is a method for safety-requirements derivation and analysis that allows for logical traceability of safety requirements through system development through to (at least) design. It uses formal refinement and requires methods from formal logics, in particular many-sorted logics that use a number of different axioms.

---

Eisenbahnregelwerke sind traditionell in natürlicher Sprache verfasst. Dies führt zu zahlreichen Problemen beim Erstellen und Verifizieren von Lasten- und Pflichtenheften und bei der unzweideutigen Spezifikation von Systemen für ein bestimmtes Betriebsverfahren. Die Ontological Hazard Analysis ist eine Methode, mit der sich durch formale Verfeinerung ("Formal Refinement") vollständige Spezifikationen der Safety-Requirements erstellen lassen. Mit Hilfe des Model-Checkers SPIN werden weitere Eigenschaften des Systems geprüft, die keine Sicherheitsanforderungen sind. Die Ontological Hazard Analysis ist, anders als gängige andere Verfahren, in der Lage, für ein echtes Bahnbetriebsverfahren eine nahtlose Nachvollziehbarkeit (audit trail) von abstrakten Spezifikationen bis zum Quellcode - abgesehen von möglichen Compilerproblemen auch bis zum Objektcode - zu bieten, und dabei gleichzeitig logische, relative Vollständigkeit der Sicherheitsanforderungen (Safety Requirements) zu garantieren.