铁路形式化方法的系统映射研究
Formal Methods in Railways: a Systematic Mapping Study
摘要：
形式化方法是基于知识的技术，用于软件密集型系统的严格开发。铁路信号领域是一个传统上应用形式化方法的领域，有几个成功的案例。本文报告了一个映射研究，调查景观的研究应用正式的方法来发展铁路系统。我们的主要结果如下：（i）我们确定了1989年至2020年期间发表的328项与我们的研究范围相关的主要研究，其中44%在过去5年内发表，24%涉及行业;（ii）大部分研究是透过例子（41%）及经验报告（38%）进行评估，而全面的个案研究则十分有限（百分之一点五）;（iii）模型检查是最常用的技术（47%），其次是仿真（27%）和定理证明（19.5%）;（四）主要语言是统一建模语言（18%）和B语言（15%），常用工具是ProB语言（9%）、NuSMV语言（8%）和UPPAAL语言（7%）;然而，使用的语言和工具多种多样;（v）大部分系统是联锁产品（40%），其次是高级控制逻辑模型（27%）;（vi）大部分研究集中在架构（66%）和详细设计（45%）开发阶段。基于这些发现，我们强调了目前的研究差距和预期的行动。特别是，需要专注于更实证的研究方法，如案例研究和控制实验，并降低抽象程度，通过应用正式的方法和工具，更接近软件开发的开发阶段。我们的研究有助于以经验为基础的角度对未来的研究和实践中正式的方法应用于铁路。
英文摘要：
Formal methods are mathematically-based techniques for the rigorous development of software-intensive systems. The railway signaling domain is a field in which formal methods have traditionally been applied, with several success stories. This article reports on a mapping study that surveys the landscape of research on applications of formal methods to the development of railway systems. Our main results are as follows: (i) we identify a total of 328 primary studies relevant to our scope published between 1989 and 2020, of which 44% published during the last 5 years and 24% involving industry; (ii) the majority of studies are evaluated through Examples (41%) and Experience Reports (38%), while full-fledged Case Studies are limited (1.5%); (iii) Model checking is the most commonly adopted technique (47%), followed by simulation (27%) and theorem proving (19.5%); (iv) the dominant languages are UML (18%) and B (15%), while frequently used tools are ProB (9%), NuSMV (8%) and UPPAAL (7%); however, a diverse landscape of languages and tools is employed; (v) the majority of systems are interlocking products (40%), followed by models of high-level control logic (27%); (vi) most of the studies focus on the Architecture (66%) and Detailed Design (45%) development phases. Based on these findings, we highlight current research gaps and expected actions. In particular, the need to focus on more empirically sound research methods, such as Case Studies and Controlled Experiments, and to lower the degree of abstraction, by applying formal methods and tools to development phases that are closer to software development. Our study contributes with an empirically based perspective on the future of research and practice in formal methods applications for railways.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
