An Engineering-Oriented Formal Framework for Railway Interlocking Systems Requirements Specifications

Hon, Yuen Man

In the German railway domain, computer-based interlocking system requirements specifications are written in natural language. It is well-known that natural language written specifications are easily misinterpreted because of their possible unclearness and ambiguity. Furthermore, checking the correctness of these specifications is difficult. Imprecise and incorrect system requirements can reduce the efficiency of a system development process and might lead to errors in the system. Using formal methods to specify system requirements in the early stage of a development process is the proposed solution to solve the stated problems. A number of research projects of applying formal methods for railway system development have been carried out. To apply these formal methods, one needs a strong mathematical background. The involvement of railway engineers in formally specifying and verifying requirements is quite limited in these projects. As a result, formal methods are not commonly used in the railway domain. The main goal of this work is to develop an engineering-oriented formal framework, such that not only computer scientists, but also railway engineers can benefit from the ideas of formal methods. The developed formal framework is called Object-Based Lastenheft (OBLH). This framework is composed of well-defined mathematical concepts and ideas for specifying, analyzing and verifying interlocking system requirements. A tool called the OBLH tool is also implemented, such that mathematical operations of these concepts can be executed automatically. The formally specified system requirements become precise and easy to be understood. Furthermore, the correctness of these requirements is also increased. In conclusion, OBLH is an engineering-oriented formal framework which can successfully bring the advantages of using formal methods to different professions.

Im Bereich des deutschen Eisenbahnverkehrs werden Anforderungsspezifikationen für elektronische Stellwerke in natürlicher Sprache verfasst. Bekanntermaßen können Spezifikationen in natürlicher Sprache aufgrund möglicher unklarer und nicht eindeutiger Formulierungen leicht falsch interpretiert werden. Außerdem gestaltet sich die Überprüfung der Korrektheit solcher Spezifikationen als schwierig. Ungenaue und inkorrekte Systemanforderungen können die Effizienz des Systementwicklungsprozesses beeinträchtigen. Sie können sogar zu Fehlern im System führen. Die Verwendung formaler Methoden zur Spezifikation dieser Systemanforderungen in einem frühen Stadium des Entwicklungsprozesses ist eine mögliche Lösung dieser Probleme. Eine Reihe von Forschungsprojekten mit diesem Schwerpunkt, Verwendung formaler Methoden, durchgeführt. Jedoch erfordert der Einsatz dieser formalen Methoden ein ausgeprägtes mathematisches Hintergrundwissen. Aus diesem Grund werden formale Methoden im Eisenbahnbereich bisher kaum eingesetzt. Das wesentliche Ziel dieser Arbeit besteht in der Entwicklung eines an den Bedürfnissen und Vorkenntnissen des Ingenieurs orientierten formalen Ansatzes und Werkzeugs, so dass nicht nur Informatiker, sondern auch Eisenbahningenieure von den Konzepten der formalen Methoden profitieren können. Der entwickelte formale Ansatz besteht in dem Objektbasierten Lastenheft (OBLH). Dieser Ansatz setzt sich aus wohldefinierten mathematischen Konzepten und Prinzipien zur Spezifikation, Analyse und Verifikation von Stellwerksystemanforderungen zusammen. Das Software-Werkzeug OBLH-Tool wurde implementiert, so dass die mathematischen Operationen dieser Konzepte automatisch ausführbar sind. Die formal spezifizierten Systemanforderungen werden dadurch klarer und sind einfach zu verstehen. Weiterhin wird die Korrektheit der Anforderungen erhöht.

Vorschau

Zitieren

Zitierform:

Hon, Yuen Man: An Engineering-Oriented Formal Framework for Railway Interlocking Systems Requirements Specifications. 2009.

Zugriffsstatistik

Gesamt:
Volltextzugriffe:
Metadatenansicht:
12 Monate:
Volltextzugriffe:
Metadatenansicht:

Details anzeigen

Rechte

Nutzung und Vervielfältigung:
Alle Rechte vorbehalten

Export