铁路系统设计中形式化工具的系统性评估与可用性分析
软件工程
2021-05-14 v2 形式语言与自动机理论
摘要
形式化方法及其支撑工具在安全关键系统的开发中拥有长久的成功记录。然而，尚无单一工具成为系统设计的 dominant 解决方案。每种工具在所使用的建模语言、验证能力及其他互补特性方面互有差异，且每个开发环境都有特殊需求，需要不同的工具。这对铁路行业而言尤为棘手：该行业规范高度推荐使用形式化方法，却未对工具的选择提供实际指导。为引导企业在其具体环境中选用最合适的形式化工具，需要对当前可用工具的特性进行清晰评估。为实现这一目标，本文考量了 13 种曾用于铁路系统设计的的形式化工具，并对这些工具进行系统性评估，同时对其中 7 种工具的子集开展了涉及铁路从业者的初步可用性分析。结果结合行业最期望的方面及早期相关研究进行了讨论。尽管关注点在铁路领域，整体方法论亦可应用于类似场景。我们的研究由此贡献了一份形式化工具的系统性评估，并表明尽管图形界面欠佳，工具的可用性与成熟度并非如文献中所称的主要障碍。相反，对流程集成的支持才是大多数工具采用过程中最相关的障碍。
引用
@article{arxiv.2101.11303,
title = {Systematic Evaluation and Usability Analysis of Formal Tools for Railway System Design},
author = {Alessio Ferrari and Franco Mazzanti and Davide Basile and Maurice H. ter Beek},
journal= {arXiv preprint arXiv:2101.11303},
year = {2021}
}