Formal Modeling and Initial Analysis of the 4SECURail Case Study

TL;DR

This paper details the formal modeling and analysis of the 4SECURail case study using three different frameworks, demonstrating how diverse representations enhance understanding of system requirements.

Contribution

It introduces a methodology for formal modeling of a railway safety system using multiple frameworks, highlighting the benefits of diverse analysis approaches.

Findings

Different formal frameworks provide complementary insights.

Modeling from multiple perspectives improves system understanding.

The approach facilitates early detection of system issues.

Abstract

We present the case study developed in the context of the 4SECURail project and the approach used for its formal modeling and analysis. Starting from a simple SysML/UML behavioral model of the system requirements, three formal models have been developed using three different frameworks, namely UMC, ProB, and CADP/LNT. The paper shows how the different ways to represent and analyze the system from the three different points of view allow us to take advantage of the resulting diversity.