Formal analysis of timeliness in the RaSTA protocol

• Autorzy: Naumann Billy , Jakobs Christine , Werner Matthias

Identyfikatory

DOI

10.15439/2022F176

• Konferencja: Federated Conference on Computer Science and Information Systems (17 ; 04-07.09.2022 ; Sofia, Bulgaria)
• Języki publikacji: EN

Abstrakty

EN

Formal reasoning about the correctness of safety-critical system's properties is crucial since such systems may impact their environment when malfunctioning. The Rail Safe Transport Application (RaSTA) Protocol is a protocol for such systems used in railway applications such as signaling. It claims to provide highly available and timely communication based on the application's demands. We investigate timeliness, i.e. the property that application data do not become obsolete. We analyze the protocol's specification and provide assumptions necessary to resolve imprecisions. Under the specified error model, we find that the deadline's proposed bound until which messages are considered timely is to restrictive, disabling RaSTA's own mechanisms to recover from lost messages in time. We formalize the specification of timeliness to provide a counterexample for the proposed bound and create an improved bound that does not lead to violated deadlines under the same assumptions and error model.

• Wydawca: Polskie Towarzystwo Informatyczne
• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2022
• Tom: Vol. 30
• Strony: 505--514
• Opis fizyczny: Bibliogr. 14 poz.

Twórcy

autor

Naumann Billy

autor

Jakobs Christine

autor

Werner Matthias