When targeting modern parallel hardware architectures, constructing correct and high-performing software is complex and time-consuming. In particular, reorderings of memory accesses that violate intended sequentially consistent behaviour are a major source of bugs. Applying synchronisation mechanisms to repair these should be done sparingly, as they negatively impact performance. In this work, we propose a technique …continue reading

ERTMS Hybrid Level 3 is a recent proposal for a train control system specification that serves to increase the capacity of the railway network by allowing multiple trains on a single track section. We have formally modelled and analysed the principles of ERTMS Hybrid Level 3 in mCRL2. Our analysis has resulted in suggestions for …continue reading