一种ARINC653文件系统服务的建模、验证和代码转换方法

摘要

随着安全关键软件规模越来越大,结构越来越复杂,高安全性的保证、验证成本高和开发周期长成为了安全关键软件开发的最主要问题.为了解决这些问题,国际上逐渐出现了一些主流的开发审定标准:美国航空无线电技术委员会(RCTA)针对安全关键软件的开发和审定所发布的DO-178B/C标准;美国航空无线电公司(ARINC)提出的航空电子应用软件标准接口(ARINC653).本文遵循D0178-CA级软件开发标准,提出了一套ARINC 653文件系统服务建模、验证和代码转换方法.首先,对ARINC 653的文件系统高层需求描述为前后置条件形式;之后使用M*抽象语言对文件系统进行建模;通过基于语境的一致性验证方法证明低层需求和高层需求的一致性;最后通过层级编码的方法将M*代码转换为MISRA-C源代码,并保证可追踪性.