Non-Deterministic Bitwise Programming to Solve the Eurobalise Telegram Encoding Problem
Sergey Mikhailovich Staroletov · Transportation research procedia · 2023
Eurobalise is a transmitter placed on railroad tracks to transmit information on a railway state to a passing train. The transmitted messages are here called Eurobalise telegrams. To transmit telegrams over the air, it is necessary to provide error-resistant encoding and corresponding decoding, which is carried out in accordance with an open standard. In this article, we continue our study of encoding such telegrams using languages with formal semantics intended for verification purposes. We present ways to apply non-deterministic programming for this task and discuss issues of implementing an encoder in the Promela language.