安全关键操作系统标准的事件驱动形式化：基于 Event-B 的 ARINC 653 经验报告
软件工程
2015-09-11 v2
摘要
标准在安全关键系统中扮演关键角色。标准中的错误可能会误导系统开发者的理解，并将缺陷引入系统实现中。在本文中，我们提出了对 ARINC 653 标准的 Event-B 形式化与验证，该标准为安全关键实时操作系统与应用软件之间提供标准化接口，以及一系列旨在提高此类安全关键系统安全性与认证过程的功能。该形式化是 ARINC 653 的完整模型，并为符合 ARINC 653 的操作系统与应用的形式化开发与验证提供了必要基础。通过使用 Event-B 形式化推理方法进行验证，发现了六个隐藏错误。
引用
@article{arxiv.1508.06479,
title = {Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B},
author = {Yongwang Zhao and Zhibin Yang and David Sanan and Yang Liu},
journal= {arXiv preprint arXiv:1508.06479},
year = {2015}
}
备注
12 pages