Towards Modeling and Verification of Eurobalise Telegram Encoding Algorithm
Sergey Mikhailovich Staroletov · Transportation research procedia · 2022
A eurobalise is designed to broadcast the current state of the railway to a passing train. Such a transmitter is activated with an approaching train and its goal is to dispatch messages called telegrams. In this article, we consider the encoding process of such telegrams. Since the CRC checksum building method is based on operations with polynomials over the Galois field modulo 2, we describe a proven library to work with polynomials. Next, we present the implementation of the encoder in a modeling language according to the open specification and then discuss its verification strategies using the Model Checking method.