Anton Wijs: “Check Your Locks and Fences: Integrating Model Checking into Fence and Transaction Insertion Analysis”
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
Bas Luttik: Modelling and Analysing ERTMS Hybrid Level 3 with the mCRL2 toolset
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