Formal Modelling and Analysis of the 4SECURail Case Study

Organisation:	ISTI/CNR, Pisa (ITALY)
Method:	UML LNT
Tools used:	ProB UMC CADP (Construction and Analysis of Distributed Processes)
Domain:	Railways.
Period:	2022
Size:	about 4000 lines of LNT 84,883,327 states
Description:	One of the goals of the 4SECURail project is to observe the possible approaches, benefits, limits, and costs of introducing formal methods inside the requirements definition process in the context of railway-signaling systems. To this aim, a "demonstrator" was set, with the purpose to exemplify the application of state-of-the-art tools and methodologies to a selected railway case study with the collection of meaningful information on the costs and benefits of the process. The transit of a train from an area supervised by a Radio Block Centre (RBC) to an adjacent area supervised by another RBC occurs during the so-called RBC-RBC handover phase and requires the exchange of information between the two RBCs via the communication layer specified within the UNISIG standards SUBSET-039, SUBSET-098, and SUBSET-037. The 4SECURail case study is based on two main sub-components of the communication layers constituting the RBC-RBC handover. The executable UML system diagrams corresponding to a given scenario are translated into the notation accepted by the UMC tool. The UMC model is then translated automatically into ProB and LNT models. The models and scenarios have been developed incrementally, with a long sequence of refinements and extensions. These automatic translations enabled the designers, at every single step, to quickly perform the lightweight formal verifications of interest with almost no effort. The focus of the formal analysis was to show how formal methods may be of help in detecting the design errors potentially introduced while producing the UML executable model, in verifying the high-level properties expected by the full system and by its specific components, and in generating clear and rigorous (graphical) feedback on the specified system to the requirements designers. The following features have been the most used during the verification experiments: static analysis in UMC/ProB/LNT, explanations and animations in UMC/ProB, weak-complete-divergence-sensitive-trace generation in UMC, fast state-space generation in UMC, divbranching minimizations in CADP.
Conclusions:	Formal analysis of an evolving requirements specification (in the elicitation and validation phases) can benefit from the possibility to exploit the analysis features offered by several verification frameworks. The automatic generation of formal models to be analyzed from some executable, standard notation makes the analysis process accessible also to people with relevant railway-signaling knowledge. The formal methods diversity approach has shown how a lightweight use of formal verification frameworks can already, with a small effort, produce important feedback on the quality of the design.
Publications:	[Mazzanti-Belli-22-a] Franco Mazzanti and Dimitri Belli. "Formal Modelling and Initial Analysis of the 4SECURail Case Study". Proc. of the 5th Workshop on Models for Formal Analysis of Real Systems (MARS'2022), EPTCS vol. 355, pp. 118-144, 2022. Available on-line at: https://arxiv.org/abs/2203.10903 or from the CADP Web site in PDF or PostScript [Mazzanti-Belli-22-b] Franco Mazzanti and Dimitri Belli. "The 4SECURail Formal Methods Demonstrator". Proc. of the 4th International Conference on Reliability, Safety and Security of Railway Systems (RSSRail'2022), LNCS vol. 13294, pp. 149-165. Springer Verlag, 2022. Available on-line at: https://www.researchgate.net/publication/360723025_The_4SECURail_Formal_Methods_Demonstrator or from the CADP Web site in PDF or PostScript
Contact:	Franco Mazzanti Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo", CNR Via G. Moruzzi 1 56124 Pisa ITALY Email: [email protected]
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page