• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>IEEE transactions on industrial informatics >Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement
【24h】

Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement

机译：集成本体和优化的分区操作系统的正式规范和分析

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Partitioning operating systems (POSs) have been widely applied in safety-critical domains from aerospace to automotive. In order to improve the safety and the certification process of POSs, the ARINC 653 standard has been developed and complied with by the mainstream POSs. Rigorous formalization of ARINC 653 can reveal hidden errors in this standard and provide a necessary foundation for formal verification of POSs and ARINC 653 applications. For the purpose of reusability and efficiency, a novel methodology by integrating ontology and refinement is proposed to formally specify and analyze POSs in this paper. An ontology of POSs is developed as an intermediate model between informal descriptions of ARINC 653 and the formal specification in Event-B. A semiautomatic translation from the ontology and ARINC 653 into Event-B is implemented, which leads to a complete Event-B specification for ARINC 653 compliant POSs. During the formal analysis, six hidden errors in ARINC 653 have been discovered and fixed in the Event-B specification. We also validate the existence of these errors in two open-source POSs, i.e., XtratuM and POK. By introducing the ontology, the degree of automatic verification of the Event-B specification reaches a higher level.
机译：分区操作系统（POS）已广泛应用于从航空航天到汽车的安全关键领域。为了提高POS的安全性和认证过程，ARINC 653标准已经被主流POS制定并遵守。 ARINC 653的严格形式化可以揭示此标准中的隐藏错误，并为POS和ARINC 653应用程序的形式验证提供必要的基础。出于可重用性和效率的目的，本文提出了一种结合本体和细化的新方法来正式指定和分析POS。 POS本体被开发为ARINC 653非正式描述与Event-B中正式规范之间的中间模型。实现了从本体和ARINC 653到事件B的半自动转换，这导致了符合ARINC 653的POS的完整事件B规范。在形式分析期间，已发现ARINC 653中的六个隐藏错误，并在Event-B规范中对其进行了修复。我们还验证了XtratuM和POK这两个开源POS中是否存在这些错误。通过引入本体，Event-B规范的自动验证程度达到了更高的水平。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号