Formal Verification for Inter-Partitions Communication of RTOS Supporting IMA

被引：1

作者：

Park, Sachoun ^{[2
]}

Kwon, Gihwon ^{[1
]}

机构：

[1] Kyonggi Univ, Dept Comp Sci, Suwon, South Korea

[2] Elect & Telecommun Res Inst, Taejon, South Korea

来源：

FRONTIER AND INNOVATION IN FUTURE COMPUTING AND COMMUNICATIONS | 2014年 / 301卷

关键词：

D O I：

10.1007/978-94-017-8798-7_50

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The IMA (Integrated Modular Avionics) architecture is widely used to support multi avionics applications and execute those applications independently. It is important to ensure the fault containment and ease of verification and certification in IMA. However during the inter-partitions communication, because it is performed by copying a message between kernel memory areas, it is possible to break the wall to prevent any partitioned function from causing a failure in another partitioned function. In this paper, we show the possibility of the error propagation in the IMA and verify the properties in the inter-partition communication module of Qplus-653 kernel.

引用

页码：415 / 421

页数：7