[转载]嵌入式系统 | Ansys SCADE在航天自动运载飞船中的应用

^Vc(oa&;  
原创 Ansys中国 沈轶烨 wwa)VgoS[  
1dy"  
JRtDjZ4>  
近期，嵌入式系统专题中我们对Ansys SCADE应用在航空电传飞控系统、轨交列车控制系统中的应用做了相关介绍。本期将为大家带来航天公司Astrium在自动运载飞船项目上应用SCADE的经验分享，其后Astrium又参与了欧洲旨在探索和研究安全关键领域如何简化形式化方法应用的Hi-Lite项目，进而将SCADE建模技术与Ada SPARK编码技术结合起来，形成了完整的从模型到代码的形式化的开发流程。 pYUQSsqC  
LzEH&y_O  
mD?={*7%  
在2013年前，Astrium是欧洲航空防务与航天公司(EADS: European Aeronautic Defence and Space Company)的一家子公司，主要提供航天民用和军事系统及相关服务。Astrium在法国，德国，英国，西班牙和荷兰都有分部。2012年的营收为58亿欧元。 69odE+-X.  
N{Pa&/V  
HMKogGTTo  
Te^_gdf  
A5ckosYyNA  
2013年末，鉴于AIRBUS的品牌知名度极高，EADS集团遂更名为AIRBUS Group。新组建的AIRBUS集团下辖3个业务部门：分别是负责民用飞机业务的Airbus，负责直升机业务的Airbus Helicopters和负责防务和航天业务的Airbus Defence & Space。其中的空客防务和航天分部是由Cassidian与Astrium合并组成。 2,h]Y=.s  
@'J[T:e  
>#.
du}t  
Astrium比较知名的业务有欧洲航天局(ESA: European Space Agency)主持的阿丽亚娜火箭(Ariane)的子系统、卫星、欧洲航天局(ESA)和美国国家航空航天局(NASA: National Aeronautics and Space Administration)联合发起的火星探测车(ExoMars)、国际空间站的哥伦布号实验舱和本篇要着重介绍的自动运载飞船(ATV: Automated Transfer Vehicle)。 m^tf=O<  
h?->A#  
QbWeQ[V{  
UH5A;SrTqR  
z<cPy)F]"  
2.1、Astrium 自动运载飞船ATV简介 yOk]RB<'r  
自动运载飞船原名阿丽亚娜运载飞船Ariane Transfer Vehicle，是欧洲航天局发起的用于国际空间站(ISS: International Space Station)货物运输的消耗性货运航天器，具有较高的自主性，可自主与国际空间站交会对接。自动运载飞船由阿丽亚娜5号火箭发射到预定轨道，在2008年至2014年共成功运行了5次，五个自动运载飞船名称分别是Jules Verne, Johannes Kepler, Edoardo Amaldi, Albert Einstein和Georges Lemaître。自动运载飞船主要为国际空间站提供如下服务： ]<_v;Q<t  
燃料补给 +' .o  
货运交付，运输包括推进剂、水、空气、食物和科研设备等各种有效载荷 W{]r_`=:6S  
国际空间站的轨道修正 uxW<Eh4H*  
国际空间站的垃圾收集与销毁 i$!K{H1{9  
k/Ao?R=@gI  
O&dh<  
97}l`z;Z  
Ff[GR$m
 
2.2、SCADE开发的ATV软件 "Z-YZ>2  
自动运载飞船的安全关键模块的软件开发使用了SCADE，最初是使用版本V3。 2kFP;7FO  
图为SCADE中定义的类型、常量、软件架构和可激活块。 xu'b@G}12  
t6%zfm   
5N2`e3:I  
^|cax|
>  
SCADE定义的状态机层级、子状态机。 _Vt CC
/  
"@jYZm8  
J$yJ2G  
建模完毕后，除了传统的验证活动外，Astrium公司还使用了法国国家科研中心(CNRS)以嵌入式系统研究著称的VERIMAG实验室的工具LESAR进行基于SCADE模型的形式化分析。LESAR工作原理同后期SCADE内嵌入的Prover工具一样。(可参考 嵌入式系统 | 基于SCADE模型的形式化方法 一文)。最后将SCADE模型生成代码，在项目中应用。 S<w?,Z  
J p0j  
S^5Qhv  
J@4 Z+l9  
2013年Astrium参与了欧洲启动的旨在探索和研究安全关键领域如何简化形式化方法应用的Hi-Lite项目。在该合作中Astrium重用了ATV项目中的SCADE模型，并结合基于Ada的SPAKR代码的形式化分析方法，进行了技术验证，获取了一定的成果。下面对此进行简要介绍。 0(A&m ,  
*Oh]I|?  
o
fCN[u  
j>hBNz  
3.1、Ada背景 92/_!P>  
Ada是20世纪70年代末美国国防部为了解决软件危机而研制的通用程序设计语言，它是以Pascal语言为基础开发实现的。Ada既继承了众多优秀高级语言的先进思想与技术，同时又融合了C++等流行语言的功能。Ada广泛应用于安全关键领域的、长生命周期的大型软件研发，在军事、商业、公共交通、金融等领域的核心软件开发中发挥着重要作用。迄今为止，国际标准组织先后确立过Ada 83,Ada 95,Ada 2005和Ada 2012共4个语言标准。取名Ada是为了纪念世界上第一位程序员Augusta Ada Lovelace女士。 _=I&zUF  
L^ U.h  
3.2、强大的断言与契约 [O3)s]|  
20世纪70年代，C.A.R.Hoare提出了著名的Hoare逻辑并由此将断言(Assertion)机制运用在程序设计语言中。断言是指在适当的程序点添加预测语句并保证程序运行时刻预测语句一定成立。断言机制的应用为保障程序正确性与提高程序可维护性提供了重要手段。例如，程序设计语言Euclid为构建可验证的系统程序而设计，其既允许将断言以注释的形式交给验证器进行处理，也允许将断言写成布尔表达式交由编译器进行编译，Euclid中的断言成为验证程序的重要手段。 |q\Rvt$d  
% )}rQqQ  
随着断言机制在程序设计语言中的成功使用，基于断言而产生的契约式设计思想于20世纪90年代被提出。与断言相比，契约式设计的层次更高，概念也更加完善，可以看作一种软件设计方法，这种方法要求软件设计者为软件组件定义形式化的、精确的、可验证的接口，从而为传统的抽象数据类型又增加了前置条件、后置条件和不变式。 lygv#s-T  
)u=a+T  
契约式编程是契约式设计在程序设计语言上的应用，不仅为程序正确性和可维护性提供了保障，同时也是减少大型软件开发成本的有效手段。 r{Z4ifSl(  
A=wh&X  
3.3、SPARK语言 };>~P%u32  
SPARK语言是一种基于Ada语言的形式化的计算机编程语言，适用于开发可预测的高可靠性的安全关键软件。20世纪90年代，Praxis公司主持设计了第一个正式将契约机制与Ada程序设计语言进行组合而产生的SPARK程序设计语言。如今，SPARK被应用在空中管制系统等高安全性要求的领域。 ^`9O$.'@  
i6:O9Km  
针对Ada 83，Ada 95和Ada 2005分别对应SPARK 83，SPARK 95和SPARK 2005三个版本。SPARK语言的第四版是基于Ada 2012的SPARK 2014，该版本对语言和支持的验证工具进行了重新设计。SPARK由一种编程语言，一个验证工具集和一种设计方法共同构成，可确保将超低缺陷软件部署在必须确保高可靠性的安全关键应用程序中。 5^{).fig  
W3B:)<f  
*adwCiB  
RJD(c#r$  
鉴于SPARK语言的成功实践，WG9委员会的专家经过多番讨论最终决定在Ada 2012中正式加入契约机制。Ada 2012中的契约由前置条件、后置条件、类型不变式和子类型谓词等概念组成，可用于类型检查、类型预测以及子程序维护等方面。另外，Ada 2012还允许在程序编程加入断言对程序的执行状态进行动态检测。 Xc
G   
DC'L-]#<  
SPARK 2014对契约使用相同的语法，这意味着用SPARK 2014验证工具可以验证用Ada 2012编写的程序，而不必重写契约。SPARK和完整Ada的子程序现在可以更轻松地共存。 M{XBmDfN  
l+^4y_  
:-T[)Q+-3  
:CXm@yF~4=  
相比老版本Ada，SPARK 2014版本增加了自己aspect以进一步帮助静态分析，这是对未经编译或执行的源代码进行的验证。验证使用执行静态分析的工具。这些工具可以采取各种形式，包括类型检查和执行可见性规则的工具(例如编译器)，以及执行更复杂的推理(例如抽象解释)的工具，如AdaCore的CodePeer之类的工具 。SPARK附带的工具执行两种不同形式的静态分析： c&#B1NN<  
A4TW`g_zm  
Flow analysis是最快的分析形式。它检查变量的初始化，并查看子程序的输入和输出之间的数据依赖性。它还可以找到未使用的赋值和未修改的变量。 =$< .:b  
proof检查是否存在运行时错误以及程序是否符合其规范。 Ot~buf'|  
6J3<k(#:  
3.4、GNAT编译器 >\s+A2P  
GNAT是Ada编程语言的免费软件编译器，它属于GNU编译器集合(GCC)的一部分。它支持Ada语言的所有版本，即Ada 83,Ada 95,Ada 2005和Ada 2012。GNAT项目始于1992年，当时的美国空军授予了纽约大学(NYU)一份合同，为Ada构建免费的编译器，以帮助Ada 9X标准化。GNAT的开发团队后来成立了两家公司，但始终是一个实体，2012年统一为AdaCore公司。 p!`S]\XEB  
wQOIUvd  
3.5、GNATprove验证工具 edfb7prfTl  
形式化验证SPARK语言的工具称为 GNATprove。它检查与SPARK子集的一致性，并执行源代码的flow analysis和proof检查。其他几种工具也支持SPARK语言，包括GNAT编译器和GPS集成开发环境。GNATprove是后面将要介绍的Hi-Lite项目的一部分，是Ada的一个形式化验证工具，它基于GNAT编译器、Why3平台和Alt Ergo prover。它可以证明子程序符合它们的契约。GNATprove目前可用于x86 linux、x86 windows和x86-64 linu K'U=);W  
[T2!,D.  
3.6、SPARK语言形式化验证的简单案例 kclZ+E  
Ada程序通常包含两个文件： #8B4*gAM  
扩展名为ads的规范文件，包含契约，契约是用aspect编写，体现了子程序的若干属性 &^F'ME  
扩展名为adb的实现文件 JuRx>F4  
AhNz[A  
仅以一个简单案例说明使用SPARK aspects来验证Ada子程序的契约。该子程序名称为Increment，作用是将参数x加1。 <im<0;i&e  
SPARK的Global aspect要求Increment子程序不读写任何全局变量 p3cb_  
SAPRK的Depend aspect要求参数x的调用仅依赖于调用前的x G;^,T/q47  
Ada的Pre和Post两个aspect定义了Increment子程序的功能属性 %$+bO/f  
Pre aspect: 仅当x值小于Integer’Last时，Increment才可被调用。这确保子程序主体中的加法操作不会溢出。 D.x&N~-  
Post aspect: x真的进行加法操作后，确保x比运算前的值大1 @`rC2-V  
4{ED~w|  
])Z p|?Y  
eeOG(@@o(  
GNATprove可验证这些契约。此外，它还可验证执行Increment子程序时不会引起运行时错误。 EzXi*/  
-N1X=4/fg  
N/8B@}@n  
?#/~BZR!  
3.7、SCADE与SPARK 5Ln !>,  
SCADE R18及其以后版本的代码生成器KCG 6.6支持将模型生成与SPARK 95版本兼容的Ada代码。Suite KCG 6.6版本的Ada代码生成器可通过DO-178C/DO-330 TQL-1等安全关键领域的工具鉴定。 slG%o5|m  
!/EN  
X[1w(dU[  
s[u*~A  
4.1、Hi-Lite项目简介 E*#5OT  
Hi-Lite项目中开发工具由参与的所有合作伙伴(学术，工具开发者和最终用户)自行指定，目的是验证在真实项目中验证形式化工具的实施情况。项目内容可以在下面列出的网址上查阅。 ce1U}">11
 
http://www.open-do.org/projects/hi-lite/ H:`H4S}  
d{c06(#_  
Hi-Lite项目定义了三个典型案例来进行研究，分别代表了不同的应用领域 BBRZlx  
航天领域：Hi-Lite工具在Astrium案例研究中的应用 .2*h!d)E  
功能安全与信息安全领域：Hi-Lite工具在各种不同SPARK示例和Tokeneer上的应用 3^Z@fC  
终端用户领域(Thales)：在面向组件的关键中间件的应用和工具集成 f.ws\^v%  
idY Xv)R  
对于每个研究的案例又都分为两个部分，1.描述案例的主要特征，2.总结使用Hi-Lite方法的益处。本篇着重介绍航天领域的案例，即由Astrium Space Transportation参与的研究，其结论是：在航天软件甚至更普遍的安全关键实时嵌入式软件中，形式化方法中是适用的。 &MJ`rj[%  
mS &^xWPV  
Astrium案例的目标和达到目标所遵循的方法 BVxk}#d  
根据欧洲航天领域的适用标准(欧洲空间合作组织标准化ECSS: European Cooperation for Space Standardization)，安全关键的实时嵌入式软件的开发人员应该对详细设计软件和对应的测试程序进行归档。Hi-Lite项目的目标是1.研究对“详细设计”进行形式化表述的方法和2.改进“形式化单元测试(Unitary Test)”的工具。 8AmB0W>e  
最初，由Astrium Space Transportation开发的每个软件子程序(subprogram)是以非形式化方式的文本进行描述的，然后通过契约进行形式化表述为： iY3TB|tMt  
|DXi~  
在何种条件下子程序可以被调用(前置条件) f(*iagEy  
子程序的预期行为(后置条件)，为了后续步骤(测试用例的描述)的方便，后置条件应尽可能地分解 1 o\COnt  
xZ`h8  
为了沿用典型的测试流程，子程序的测试用例以非形式化地描述。测试用例的定义应该与详细设计时测试用例的定义兼容。 S+-V16{i  
测试用例在SPARK 2014中形式化 D#d \1g  
详细设计和测试用例(两者都以SPARK 2014格式进行形式化)的评审应该作为详细设计评审(DDR: Detailed Design Review)和测试就绪评审(TRR: Test Readiness Review )的一部分 ,TQ;DxB}=E  
每个测试用例或者被形式化证明，或者被测试 Wf-Pa9  
测试规程被定义 lxtt+R  
Q6%Pp_$k  
应该确保覆盖率： ?q}:ojrs1  
软件需求和详细设计的覆盖 &nwk]+,0W#  
详细设计与测试规程的覆盖 '17V7A/t  
dY.NQ1@"  
4.2、Astrium Space Transportation的案例内容 ~{{@m]P  
典型的太空飞行程序大致由4个部分组成： ;b0;66C8|  
底层软件，操作系统，驱动程序。这些软件不在Hi-Lite考察范围内 0Q:l,\lY  
数据管理，此类软件的典型应用是遥测和遥控，因为主要涉及对数据进行编码和解码，经分析也不太适合Hi-Lite研究 \S)cVp)h  
飞行控制或更一般的数值控制/指令算法 ME'LZ"VT  
任务和飞船管理 W-4R;!42  
mC!^`y)  
Astrium的Hi-Lite项目主要涉及后面两项。由于仅第三部分的飞行控制或更一般的数值控制/指令算法用到了SCADE模型，下面几节主要对此作介绍。 Eyg F,>.4  
t^g+nguz  
4.3、数值控制/指令算法案例的设计 c^}DBvG,  
数控/指令算法案例将浮点值作为输入，执行一些数值计算(使用经典的基本数学运算符，例如加法，减法，乘法，除法，绝对值，三角函数或对向量和数组的运算等)并返回浮点型结果。这样算法通常具有诸如内部状态等上下文环境。 (6X{ &  
Ca#T?HL  
一般来说，定义精确的功能规约这些技术对这类代码毫无用武之地。例如方程的功能规约X := A * Y + Cos(Z)就是表达式本身，几乎不可能以更抽象的方法定义该公式。舍去精化公式的工作后，研究目的就是证明这类公式没有运行时错误(例如除0)和确保范围的正确性(例如，速度应该始终在0~25km/s之间)。 o(oD8Ni  
3u1\zse  
其中的太阳能帆板管理软件(可用于ATV)就是以数值控制/指令算法为基础实现的。该软件负责 p1 mY!&e(  
部署太阳能帆板(通过控制硬件链接来收放) LTnbBh*mc  
调整太阳能帆板的方位来优化接收的太阳能 NnO%D^P]  
@eN,m {b  
太阳能帆板部署功能是用SCADE建模的，并用认证级的SCADE KCG Ada工具自动生成与SPARK兼容的代码。SCADE建模、验证、代码生成等阶段工作完毕后，接下来就需要评估Hi-Lite工具集分析自动生成代码的能力。从SCADE模型生成的代码示例如下: ic?(`6N8  
j%fi*2uX  
-}"nb-RR\  
}n?D#Pk,  
太阳能帆板的方位控制功能是手工编码的，也需要评估Hi-Lite工具集分析算法手工代码的能力。该部分代码使用了数学库，不过数学库并非全部由SPARK 2014实现，即该部分不能形式化证明，只能进行常规测试。幸好数学库的接口是符合SPARK 2014的，因此可用形式化方法证明上层的应用程序代码。 RtF!(gd  
>$;,1N $bd  
数学库契约的示例如下： BYb"[qPV  
D]+@pKb  
v)LSH;<  
F|?}r3{aJ  
E&> 2=$~  
应用程序代码中定义的契约仅与变量范围有关，示例如下： 1cd3m  
FdS'0#$  
O2oF\E_6  
8l>YpS*S^  
Z#s-(wf  
smqUFo  
4.4 、数值控制/指令算法案例的证明 %H=^U
8WB  
所有契约均通过了动态测试检查。然后是使用gnatprove进行形式化证明。如前述，证明两部分 t9&=; s  
Mathematical_Library m%)S<L7 l  
Numerical_Algorithms LBnlaH.  
!+n'0{  
Mathematical_Library的结果 O]Q8&(  
分析用时为233秒(3分53秒)。下表为子程序数量，分为3种：由SPARK 2014设计，非SPARK 2014设计和部分由SPARK 2014设计 G PL^!_  
XPMvAZL  
Y|-:z@n6C  
下表为验证条件VC(Verification Condition)的分析，列的主要内容为 fs8C ^Ik>~  
VC被证明的数量 8D`TN8[W  
VC未被证明的数量 Cuo"6, M  
百分比(VC证明和未被证明的) +D M,+{}  
总数 OwLJS5r@<-  
.8]=yPm  
Dx.hM[  
pzxlh(a9  
关于未被证明的VC的原因分析：某些函数算法是GNATprove不能完全理解的。例如 qex::Qf  
mJME1#j$/|  

dXDuO  
@Qd5a(5WM  
本例所示的Post契约无法通过GNATprove来证明。算法函数的精确行为取决于具体实现，这是可接受的。不能证明部分的解决方法是通过密集测试等传统方法来验证。 %WtF\p  
FES0lw{G#  
Numerical_Library的结果 ]NY^0SqM  
分析用时为653秒(10分53秒)。下表为子程序数量，分为3种，由SPARK 2014设计，非SPARK 2014设计和部分由SPARK 2014设计 Gc<^b  
Fhs/<w-  
.Iv`B:4  
下表为验证条件VC(Verification Condition)的分析，列的主要内容为 kvam`8SeL  
VC被证明的数量 lk4$c1ao2@  
VC未被证明的数量 9&1$\ZH  
百分比(VC证明和未被证明的) #kAk d-QY6  
总数 0D}k
^W  
Y$
FhV~m  
kDc/]Zb%  
M&0U@ r-  
关于未被证明的VC的原因分析有两类。 "cDc~~3/@  
第一类Assert无法证明是由于GNATprove无法处理四舍五入。 /5Xt<7vm8  
r,wC5%&Za  
z#+Sf.  
|kqRhR(Ei  
第二类Assertion无法证明，因为它是非线性运算。 $2$jV1s  
K(_8oB784  
Hx ojxZwm  
^-s`$lTp  
h BzZJ/jn  
&[$t%:`  
4.5、Astrium案例评估结果 zu``F]B  
Astrium希望评估的目标是，SPARK 2014应该满足以下需求， h{CyYsQ  
可以将测试用例形式化表述的能力 A
nQUdU  
测试规程覆盖测试用例的验证(注: 测试用例，测试规程，测试结果) D1cnf"y^  
支持验证和确认没有运行时错误 ^fti<Lw5  
支持验证和确认功能属性
uEyus96 +  
- 4B&{P  

未注册仅能浏览部分内容，查看全部内容及附件请先 登录 或 注册