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.
Software specification and development in the domain of railway signalling
2003
12 Seiten, 2 Tabellen, 13 Quellen
Aufsatz (Konferenz)
Englisch
Software Specification and Development in the Domain of Railway Signalling
British Library Conference Proceedings | 2003
|Software requirements for railway signalling systems
Tema Archiv | 1988
|Software safety technologies for railway signalling
IuD Bahn | 1999
|UML-based specification of a railway interlocking and signalling system
Tema Archiv | 2003
|Software Safety Technologies for Railway Signalling
British Library Online Contents | 1998
|