证明助手、检查器与生成器的资质认证：现状与展望
软件工程
2023-02-21 v1
摘要
信息物理系统，如学习型机器人及其他自主系统，在其安全关键控制中采用高完整性软件。该软件的开发使用了一系列工具，其中部分工具需要根据国际标准为此目的进行资质认证。本文首先通过SWOT（优势、劣势、机会、威胁）分析，评估了证明助手、检查器（如模型检查器）和生成器（如代码生成器、编译器）工具资质认证的现状。我们的重点是上述三类工具的资质认证。我们的目标是评估这些工具在何种条件下已经适合或能够变得适合用于高完整性控制软件的实际工程与保障。第二步，我们从SWOT分析的结果中得出一个观点，并提出了一系列相应的改进工具资质认证的建议。
引用
@article{arxiv.2302.09546,
title = {Qualification of Proof Assistants, Checkers, and Generators: Where Are We and What Next?},
author = {Mario Gleirscher and Robert Sachtleben and Jan Peleska},
journal= {arXiv preprint arXiv:2302.09546},
year = {2023}
}