The application of formal methods (FM) in the field of railway signalling is a great challenge for the co-operation of the academic world and the industrial specialists. Under formal methods (FM) the authors understand such procedures, in course of which mathematical notations (e.g. from the field of logic or set theory) are applied for the description of certain system properties at certain stages of the life cycle of the examined system. FM enable the formal description of certain system properties both in relation to the specification and the implementation. Thus, FM include formal specification, development, design, verification and validation techniques, based on mathematics, thus they provide the possibility to proceed the activities of the life cycle phases systematically The primary aim of the application of FM in the field of railway signalling is to provide such a tool for the customers, the developers, the specialists of the authority and the assessors, with help of which the correctness of the railway signalling systems, to be established, can be ensured and proven reliably and cost-effectively, while taking all the specialities of the given domain into account. In this paper, based on the above mentioned application aspects, guidelines will be introduced for the application of FM in the domain of railway signalling, by taking into account the specialities of this domain. Since the evaluation of administrative aspects in the field of railway signalling does not differ significantly from that of other domains, this paper deals purely with the rigor, scope and technical aspects of the application of FM. Since between single aspects of this collection strong interactions can be observed (primarily between the rigor and the scope of formalization), it is practical to take one of the aspects out as a frame for the discussion of the guidelines. The application mode of FM is mainly determined by the stage of the system life cycle, in which the authors intend to apply FM, therefore the aspect scope according to the life cycle phases will be set out as a discussion frame. If the authors examine the development process of railway signalling systems, it can be stated, that the application of FM can be grouped around two specific life cycle phases; these are the development of the customer requirements (also called Lastenheft in German) and the development of the system specification (also called Pflichtenheft in German). The application guidelines, related to these life cycle phases, will be introduced in Sections 3 and 4 respectively. Following, the transitivity between customer requirements and the system specification will be analyzed in connection with FM in Section 5. Finally, Section 6 deals with the procedure of the introduction of FM into the field of railway signalling.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Software specification and development in the domain of railway signalling


    Beteiligte:
    Saghi, B. (Autor:in) / Tarnai, G. (Autor:in)


    Erscheinungsdatum :

    2003


    Format / Umfang :

    12 Seiten, 2 Tabellen, 13 Quellen




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Software Specification and Development in the Domain of Railway Signalling

    Shagi, B. / Tarnai, G. / Zentrum fur Verkehr der Technischen Universitat Braunschweig et al. | British Library Conference Proceedings | 2003



    Software safety technologies for railway signalling

    Hirao, Yuji / Fukuda, Mitsuyoshi | IuD Bahn | 1999


    UML-based specification of a railway interlocking and signalling system

    Zahradnik, J. / Rastocny, K. / Janota, A. | Tema Archiv | 2003


    Software Safety Technologies for Railway Signalling

    Hirao, Y. / Fukuda, M. | British Library Online Contents | 1998