In: Proc. IFAC Conf. on Control Systems Design (CSD'2000), 18-20 June 2000, Bratislava, Slovak Republic, pages 275-280. 2000.
Abstract: Higher standards in performance and safety of future train control systems require the use of formal methods for the safe and efficient system development in this domain. At the beginning of each life cycle an operation method which views the train control system in its interaction with the driver and the physical process has to be developed. To describe the system dynamics, especially considering the concurrency between the vehicle and track components of the train system, Petri nets are used as formal language. This contribution considers the question what the functional requirement specifications have to contain and how they can be described formally by Petri nets. A concept of structuring for the formal specifications of operation methods is introduced which allows a systematic modeling of the permissible system behavior on the requirement level. The permissible system behavior contains the regular functions and the management of permissible faults. The concept of structuring intends to model the physical process and the train control system in different models which can then be coupled suitably. Furthermore, the train control system is decomposed into models which correspond to physical components which posesses precise communication interfaces and which are usually distributed. The engineer's view is supported by this approach and a model structure is created which leads to an unambiguous description of permissible process behavior related to the tasks of the control systems.
Keywords: Petri nets, formal specifications, operation method, railway systems, requirement analysis, train control systems.