A refinement-based development of a distributed signalling system

The decentralised railway signalling systems have a potential to increase capacity, availability and reduce maintenance costs of railway networks. However, given the safety-critical nature of railway signalling and the complexity of novel distributed signalling solutions, their safety should be guaranteed by using thorough system validation methods. To achieve such a high-level of safety assurance of these complex signalling systems, scenario-based testing methods are far from being sufficient despite that they are still widely used in the industry. Formal verification is an alternative approach which provides a rigorous approach to verifying complex systems and has been successfully used in the railway domain. Despite the successes, little work has been done in applying formal methods for distributed railway systems. In our research we are working towards a multifaceted formal development methodology of complex railway signalling systems. The methodology is based on the Event-B modelling language which provides an expressive modelling language, a stepwise development and a proof-based model verification. In this paper, we present the application of the methodology for the development and verification of a distributed protocol for reservation of railway sections. The main challenge of this work is developing a distributed protocol which ensures safety and liveness of the distributed railway system when message delays are allowed in the model.

Uma Nova Metodologia para formação de Grupos em VANETs

This work proposes a new methodology to create groups in intervehicular networks as a basis for complex applications involving smart vehicles. We proposed a distributed protocol whose purpose is to build a higher number of groups in less time, keeping the vehicles grouped for most of their journey. We implement our proposal in two versions. The first one considers only the interaction among vehicles. The second includes a group merge functionality. We validate both versions of our protocol using simulation with real traffic data. We evaluate the amount of created groups and their persistence and size.