一种基于ARINC653核心系统服务的建模和代码转换方法

摘要

ARINC653名为《航空电子应用软件标准接口》,它是具有高安全性的实时分区操作系统的标准规范.开发与验证符合ARINC653规范的高安全操作系统需要遵循RTCA(Radio and Technical Commission for Aeronautics)发布的D0-178B和D0-178C标准,即《机载系统和设备认证中的软件要求》标准.D0-178C将软件安全等级分为5个级别,E级-A级,A级为最高级别.提出一种遵循D0-178C A级安全级别的软件开发与验证方法,该方法通过建模、形式化验证和代码转换对ARINC653核心系统服务进行形式化开发和验证.本文主要就建模和代码转换予以阐述.