Ferrari A, Mazzantif., Basile D., Ter Beek M. H., Fantechi A.
Judgment study Railway Formal tools Empirical software engineering Formal methods diversity Human aspects of formal design Empirical formal methods Moving-block system Formal methods
Formal methods and tools have a long history of successful applications in the design of safety-critical railway products. However, most of the experiences focused on the application of a single method at once, and little work has been performed to compare the applicability of the different available frameworks to the railway context. As a result, companies willing to introduce formal methods in their development process have little guidance on the selection of tools that couldfi t their needs. To address this goal, this paper presents a comparison between 9 different formal tools, namely Atelier B, CADP, FDR4, NuSMV, ProB, Simulink, SPIN, UMC, and UPPAAL SMC. We performed a judgment study, involving 17 experts with experience in formal methods applied to railways. In the study, part of the experts were required to model a railway signaling problem (a moving-block train distancing system) with the different tools, and to provide feedback on their experience. The information produced was then synthesized, and the results were validated by the remaining experts. Based on the outcome of this process, we provide a synthesis that describes when to use a certain tool, and what are the problems that may be faced by modelers. Our experience shows that the different tools serve different purposes, and multiple formal methods are required to fully cover the needs of the railway system design process.
Source: ICSE'20 - 42nd International Conference on Software Engineering, pp. 62–74, Seoul, Republic of Korea, 27/6/2020-19/7/2020
Publisher: ACM Press, New York, USA
@inproceedings{oai:it.cnr:prodotti:424614, title = {Comparing formal tools for system design: a judgment study}, author = {Ferrari A and Mazzantif. and Basile D. and Ter Beek M. H. and Fantechi A.}, publisher = {ACM Press, New York, USA}, doi = {10.1145/3377811.3380373}, booktitle = {ICSE'20 - 42nd International Conference on Software Engineering, pp. 62–74, Seoul, Republic of Korea, 27/6/2020-19/7/2020}, year = {2020} }