Cyber-physical systems, such as learning robots and other autonomous systems, employ high-integrity software in their safety-critical control. This software is developed using a range of tools some of which need to be qualified for this purpose according to international standards. In this article, we first evaluate the state of the art of tool qualification for proof assistants, checkers (e.g., model checkers), and generators (e.g., code generators, compilers) by means of a SWOT (Strengths, Weaknesses, Opportunities, Threats) analysis. Our focus is on the qualification of tools in the three mentioned categories. Our objective is to assess under which conditions these tools are already fit or could be made fit for use in the practical engineering and assurance of high-integrity control software. In a second step, we derive a viewpoint and a corresponding range of suggestions for improved tool qualification from the results of our SWOT analysis.
翻译:网络物理系统(如学习型机器人及其他自主系统)在安全关键控制中采用高完整性软件。此类软件开发涉及多种工具,其中部分工具需根据国际标准为此目的进行资质认定。本文首先通过SWOT(优势、劣势、机遇、威胁)分析法评估证明助手、验证器(如模型检验器)及生成器(如代码生成器、编译器)三类工具资质认定的技术现状,重点关注这三类工具的资质认定问题。我们旨在评估这些工具在何种条件下已具备或可被改造为适用于高完整性控制软件的实际工程与保障。其次,基于SWOT分析结果,我们提炼出改进工具资质认定的观点及相应的一系列建议。