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.

In building software architectures, the relations between elements in different diagrams are often overlooked. The first stage of building IT systems is the use of ontology terminology, not software terminology, in the requirements engineering process. Then, when constructing software architecture, IT architects more or less consciously however introduce elements that represent the same classifier on different diagrams with similar names. These connections are called consistency rules and are usually not attached in any way in a modeling tool, and only a significant number of them in the models increase the quality of the software architecture. It is mathematically proved that the application of consistency rules increases the information content of software architecture. Authors show that increasing readability and ordering of software architecture by means of consistency rules have their mathematical rationale. In this article, we found proof of decreasing Shannon entropy while applying consistency rules in the construction of software architecture of IT systems. Therefore, it has been shown that marking selected elements in different diagrams with these same names is, therefore, an implicit way to increase the information content of software architecture while simultaneously improving its orderliness and readability. Moreover, this increase in the quality of the software architecture can be measured by entropy, which allows for checking whether the number of consistency rules is sufficient to compare different architectures, even of different sizes, thanks to entropy normalization, and checking during the development of the software architecture, what is the improvement in its orderliness and readability.

Transportation problems of large urban conurbations inspire search for new transportation systems that meet high environmental standards, are relatively cheap and user friendly. The latter element also includes the needs of disabled and elderly people. This article concerns a new transportation system - Personal Rapid Transit (PRT). In this article, the attention is focused on the analysis of the efficiency of the PRT transport network. The simulator of vehicle movement in PRT network as well as algorithms for traffic management and control are presented. The proposal of its physical implementation is also included.

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.