一种基于M*的ARINC653多核操作系统开发方法

摘要

随着处理器技术的发展,航空电子系统从单核走向多核是一种必然的趋势.本文提出了一种基于M*的ARINC653分区多核操作系统的实现方法,利用M*的集合操作,完成了对所有基本系统服务的建模,针对多核系统核间通信问题,提出了一种核间通信的模型.这种方法屏蔽了底层复杂的数据结构,简洁高效,为日后的形式化验证工作打下了基础.