Empty vehicles management may improve the average waiting time for vehicle delivery in the Personal Rapid Transit (PRT) network. In this study, original heuristic algorithm of empty vehicle management is presented. The algorithm is tested in several benchmark PRT structures under Feniks simulation environment. The results show that significant improvements of average waiting time may be achieved just because of the multi‐parameter analysis of the present network state alone rather than by the predictive use of forecasted demand. The algorithm does not use any central database of demand and location of free vehicles. Instead, it assumes the local exchange of data between stations on their state and expected vehicles. Therefore it seems well tailored to a distributed implementation.

The ERTMS/ETCS is the newest automatic train protection system. This is a system that supports the driver in driving the train. It is currently being implemented throughout the European Union. This system’s latest specifications also provide additional functions to increase the energy efficiency of train driving in the form of ATO (automatic train operation). These functions of the ETCS will be valuable, provided they operate without failure. To achieve errorless configuration of the ETCS, a methodology for automatic system verification using the IMDS (Integrated Model of Distributed Systems) formalism and the temporal tool Dedan was applied. The main contribution is asynchronous and timed verification, which appropriately models the distributed nature of the ETCS and allows the designer not only to analyze time dependencies but also to define the range of train velocities in which the operational scenario is valid. Additionally, the novelties of the presented verification methodology are the graphical design of the system components and automated verification freeing the designer from using textual design. We express the verified properties as observer automata rather than in temporal logic. Moreover, we check partial properties related to system fragments, which is crucial in distributed systems. This paper presents the verification of an example ETCS system application. The verification results are presented as sequence diagrams leading to a correct/incorrect final state.

Relay-based traffic control systems are still used in railway control systems. Their correctness is most often verified by manual analysis, which does not guarantee correctness in all conditions. Passenger safety, control reliability, and failure-free operation of all components require formal proof of the control system’s correctness. Formal evidence allows certification of control systems, ensuring that safety will be maintained in correct conditions and the in event of failure. The operational safety of systems in the event of component failure cannot be manually checked practically in the event of various types of damage to one component, pairs of components, etc. In the article, we describe the methodology of automated system verification using the IMDS (integrated model of distributed systems) temporal formalism and the Dedan tool. The novelty of the presented verification methodology lays in graphical design of the circuit elements, automated verification liberating the designer from using temporal logic, checking partial properties related to fragments of the circuit, and fair verification preventing the discovering of false deadlocks. The article presents the verification of an exemplary relay traffic control system in the correct case, in the case of damage to elements, and the case of an incorrect sequence of signals from the environment. The verification results are shown in the form of sequence diagrams leading to the correct/incorrect final state.

It is difficult to organize urban transport in the city center. Existing buildings, narrow streets and working infrastructure make it difficult to use the oldfashion transport means such as trams or buses. The new idea consists in elevation of the transport in the very city above ground level (typical PRT systems cover rare areas like airport or fairgrounds). The study analyzes the hierarchical, layered system consisting of a ring light rail and PRT (Personal Rapid Transit) serving as commuter network. It is shown in the case of an exemplary city that the proposed solution is possible and reasonable. Ridership and vehicle mileage of the entire system are calculated for the light rail analytically, and in the case PRT by simulation.

The aim of this paper is to demonstrate how the COSMA environment can be used for system modeling. This environment is a set of tools based on Concurrent State Machines paradigm and is developed in the Institute of Computer Science at the Warsaw University of Technology. Our demonstration example is a distributed brake control system dedicated for a railway transport. The paper shortly introduces COSMA. Next it shows how the example model can be validated by our temporal logic analyzer.Comment: 6 pages, 3 figures, 1 tabl