一种基于Arinc653操作系统的形式化建模语言

摘要

随着机载软件系统高度综合化、模块化,为了提高机载软件的安全性和可靠性,国际ARINC组织针对IMA结构提出了健壮分区的思想,并制定了ARINC653标准.为了更加简单高效的实现对ARINC653实时操作系统的建模及其验证,基于现有的形式化开发方法B,提出了一种新的形式化开发方法B*.B*基于一阶逻辑和集合论,本文主要介绍其中的建模语言B*语言.为了在抽象层次实现对ARINC653操作系统的建模,B*语言区别于常规的高级程序语言,它将数组、链表等具体的数据结构抽象成集合,以便能够在抽象层进行验证,降低建模与验证的难度.当使用B*完成系统的建模与验证,需要将B*模型转换成可执行的代码,基于下推自动机理论,实现了B*模型到C语言之间的自动转换,并对转换的语义等价性给出了形式化的证明.