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.


    Zugriff

    Download

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

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


    Weitere Titelangaben:

    Ein ingenieurgerechtes formales Verfahren für die Spezifikation von Stellwerksanforderungen


    Beteiligte:
    Hon, Yuen-Man (Autor:in) / Universitätsbibliothek Braunschweig (Gastgebende Institution) / Pachl, Jörn (Akademische:r Betreuer:in)

    Erscheinungsdatum :

    2009



    Medientyp :

    Sonstige


    Format :

    Elektronische Ressource


    Sprache :

    Englisch


    Klassifikation :

    DDC:    625