胡建成，胡 军，汪文轩，康介祥，王 辉，高忠杰

1(南京航空航天大学 计算机科学与技术学院，南京 211106)

2(软件新技术与产业化协同创新中心，南京 210007)

3(中国航空无线电电子研究所 软件部，上海 200233)

1 引 言

安全关键软件[1，2]是指应用于航空、航天、交通、能源等安全关键系统领域中的一类软件，此类软件系统要求具有高安全性、高可靠性和高健壮性等特征[3].近年来，随着安全关键系统的功能及复杂度的快速增长，以及软件很小的错误或者漏洞可能会导致非常严重的后果[4]，例如：财产的重大损失、环境的严重破坏或者是人员的重大伤亡等.因此，如何正确有效的开发此类系统软件成为了目前安全关键系统领域中的一个重要挑战.

从软件生命周期的角度来看，在一个软件产品开始的阶段定义并构造一个完整性、一致性良好的需求制品，是提高安全关键软件的产品质量和降低产品开发成本的最好方法之一.由于系统具备安全关键特征，相比较在设计或实现阶段引入的错误，在安全关键软件需求中存在的错误更可能会对这类系统的安全性产生重要影响.以航空电子系统(以下简称航电系统)中的软件系统为例，其相应的民用机载软件适航标准DO-178B/C[5]中就是以多层级需求为核心来展开航电软件研发的各类活动，并引入了最新的基于模型的系统/软件工程方法学以及形式化方法[6，7]来更好的支撑达成安全性等相关目标.

本文工作就是面向航空电子……