The Formal Development of A Railway Station Route Management System Dong Yu Lin Submitted to the Faculty of Science and Technology on May, 1995,in partial fulfilment of the requirements for the degree of Master of Science Abstract This thesis is about the formal and rigorous development of RoManS (Route Management System)for railway station route management. Route management deals with train traffic within a station, and route trains according to timetables and station layout so that smooth accident-free (somehow optimal) train trafc can be ensured. RoManS is software that can support station staff in managing routes. In this thesis,we are concerned with three main "phases": domain analysis, requirement capture and software development. Domain analysis is the process of obtaining knowledge of the environment in which the software serves; that is of all properties upon which subsequent software may have to rely in order for it to function according to expectations correctly and properly. Domain analysis must be taken as a part of software construction and is primarily pursued (and documented) prior to requirements capture. Requirement capture is now a process which, from the resulting descriptions of the domain analysis, extracts their interactions to come up with a requirements specification. Architecture design is then derived. In this design the gross structure of the system becomes apparent in terms of high-level components and connections among these components. The architecture design is then further developed into concrete design and translated into C code, A formal method, RAISE and its development methods, is applied in all of these phases. This thesis contributes to the methodology of software engineering by showing new ways of developing software. It also identified and clarified some issues in domain analysis, requirement capture and software development. Supervisor: Prof. Dr. Dines Bjørner Director The United Nations University International Institute for Software Technology