杨志斌 , 袁胜浩 , 谢 健 , 周 勇 , 陈 哲 , 薛 垒 , Jean-Paul BODEVEIX, Mamoun FILALI

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

2(软件新技术与产业化协同创新中心,江苏 南京 210093)

3(上海航天电子技术研究所,上海 201109)

4(IRIT-University of Toulouse, Toulouse 31062, France)

安全关键软件(safety-critical software)[1]是指应用于航空、航天、交通、能源等领域的安全关键系统中,且其运行情况可能引起系统处于危险状态,从而导致财产损失、环境破坏或者人员伤害的一类软件.随着功能需求的发展,能够提供更强计算能力而又能减少电子设备的体积、重量和功耗(size,weight and power,即SWaP特性)的多核处理器将在安全关键领域得到广泛应用.例如,在航空领域,风河公司(WindRiver)提出了支持多核处理器的 Vxworks 653操作系统 V3.0版本[2];而为了满足将来航天应用的复杂需求,欧空局(European Space Agency,简称ESA)开发了基于四核LEON4的下一代微处理器试验板(LEON4-N2X)[3].

近年来,模型驱动(model-driven),尤其是采用形式化模型驱动的安全关键软件设计与开发方法逐渐受到重视,并被工业界认为是切实可行的重要手段.例如,国际民航领域使用的机载系统适航审定中的软件开发标准DO-178C[4]就将模型驱动和形式化方法(即 DO-331[5]和 DO-333[6])作为其核心标准的重要技术补充.模型驱动开发方法将模型作为整个软件开发过程的核心元素,在设计阶段就建立软件模型,并尽早进行验证和分析.同时,模型的重用以及基于模型的自动代码生成,都有助于降低软件开发时间和成本.

安全关键系统,是一类反应式系统(reactive system),它不断地和环境进行交互,即从环境中得到输入,经过计算,然后输……