形式化方法在铁路领域的系统映射研究
软件工程
2022-02-28 v2
摘要
形式化方法是以数学为基础、用于严谨开发软件密集型系统的技术。铁路信号领域是传统上应用形式化方法并拥有若干成功案例的一个领域。本文报道了一项映射研究,调查了形式化方法应用于铁路系统开发的研究全景。我们的主要结果如下:(i)我们确定了1989至2020年间与我们的范围相关的328篇主要研究,其中44%发表于最近5年,24%涉及工业界;(ii)大多数研究通过示例(41%)和经验报告(38%)进行评估,而完整的案例研究有限(1.5%);(iii)模型检测是最常采用的技术(47%),其次是仿真(27%)和定理证明(19.5%);(iv)主导语言为UML(18%)和B(15%),而常用工具为ProB(9%)、NuSMV(8%)和UPPAAL(7%);然而,所采用的语言和工具呈现多样化局面;(v)大多数系统为联锁产品(40%),其次为高层控制逻辑模型(27%);(vi)大多数研究聚焦于架构(66%)和详细设计(45%)开发阶段。基于这些发现,我们指出了当前的研究空白和预期的行动。特别地,需要聚焦于更具实证可靠性的研究方法,如案例研究和受控实验,并通过将形式化方法和工具应用于更贴近软件开发的开发阶段来降低抽象程度。我们的研究为铁路形式化方法应用的未来研究和实践提供了基于实证的视角。
引用
@article{arxiv.2107.05413,
title = {Formal Methods in Railways: a Systematic Mapping Study},
author = {Alessio Ferrari and Maurice H. ter Beek},
journal= {arXiv preprint arXiv:2107.05413},
year = {2022}
}