Write a Blog >>
ICSE 2020
Wed 24 June - Thu 16 July 2020
Tue 7 Jul 2020 16:17 - 16:29 at Baekje - A4-Cyber-Physical Systems Chair(s): Joanne M. Atlee

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 could fit 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 signalling problem (the moving-block train distancing system) with the different tools, and to provide feedback on their experience. The information produced was then synthesised, 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 modellers. 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.

Tue 7 Jul
Times are displayed in time zone: (UTC) Coordinated Universal Time change

16:05 - 17:05: Paper Presentations - A4-Cyber-Physical Systems at Baekje
Chair(s): Joanne M. AtleeUniversity of Waterloo
icse-2020-papers16:05 - 16:17
Dalal AlrajehImperial College London, Antoine CailliauICTEAM, UCLouvain, Axel van LamsweerdeUniversité catholique de Louvain
icse-2020-papers16:17 - 16:29
Alessio FerrariCNR-ISTI, Franco MazzantiISTI-CNR, Davide BasileUniversity of Florence, Maurice H. ter BeekISTI-CNR, Alessandro FantechiUniversity of Florence
DOI Pre-print
Demonstrations16:29 - 16:32
Shafiul Azam ChowdhuryUniversity of Texas at Arlington, Sohil Lal ShresthaThe University of Texas at Arlington, Taylor T JohnsonVanderbilt University, Christoph CsallnerUniversity of Texas at Arlington
Link to publication DOI Media Attached
icse-2020-Software-Engineering-in-Practice16:32 - 16:44
Anders Fischer-NielsenIT University of Copenhagen, Zhoulai FuIT University of Copenhagen, Denmark, Ting SuETH Zurich, Switzerland, Andrzej WąsowskiIT University of Copenhagen, Denmark
Demonstrations16:44 - 16:47
Sergio GarciaChalmers | University of Gothenburg, Patrizio PelliccioneUniversity of L'Aquila and Chalmers | University of Gothenburg, Claudio MenghiUniversity of Luxembourg, Thorsten BergerChalmers | University of Gothenburg, Tomas BuresCharles University, Czech Republic
icse-2020-Software-Engineering-in-Practice16:47 - 16:59
Ivano MalavoltaVrije Universiteit Amsterdam, Grace LewisCarnegie Mellon Software Engineering Institute, Bradley SchmerlCarnegie Mellon University, USA, Patricia LagoVrije Universiteit Amsterdam, David GarlanCarnegie Mellon University