[转载]嵌入式系统 | Ansys SCADE在航空项目利勃海尔中的应用

),y{.n:wm  
原创 Ansys中国 沈轶烨 #`)zD"CO  
o%X@Bz  
Ansys中国系统事业部推出的<嵌入式系统>专题中，已陆续为大家带来六期精彩内容，分别对Ansys SCADE在核电项目、航空电传飞控系统、轨交列车控制系统以及航天防卫中的应用做了详细介绍。本期将分享其在航空项目利勃海尔的应用案例。本文第1、2节简要介绍了利勃海尔公司及其综合空气管理系统，第3节介绍了Ansys SCADE在利勃海尔综合空气管理系统开发中的应用，第4节介绍利勃海尔团队提出的形式化方法辅助生成测试规程的流程，最后带来相关案例介绍。 -Wc'k 2oU  
VU`aH9g3(  
B;?)   
成立于1949年的德国家族企业利勃海尔集团(Liebherr)在2018年的营收首次突破100亿欧元。尽管利勃海尔集团的产品是借战后德国重建的契机，以移动塔式起重机起家，但凭借创始人汉斯·利勃海尔(Hans Liebherr)精准的眼光与卓越的能力，逐步将业务拓展到包括家用电器，工程机械，轨道交通和航空航天领域。 x0B|CO  
(5rH72g(  
利勃海尔是在1950年代末从维修军用飞机起落架开始涉足航空领域的，今天利勃海尔的航空和运输系统部门生产的起落架系统(landing gears system)、空气管理系统(air management system)和飞行控制系统(flight control system)早已蜚声业内，成为航空业全球领先的系统供应商之一。 8xzEbRNJ)  
vQ"EI1=7Z  
国产C919飞机的综合起落架系统就是由利勃海尔位于德国林登堡的航空部门(Liebherr-Aerospace Lindenberg GmbH) 负责制造的。而国产C919飞机的综合空气管理系统，则是由利勃海尔位于法国图卢兹的航空部门(Liebherr-Aerospace Toulouse SAS)负责制造。 4
.2qt  

#n5q$  
)B.NV<m  
I)I,{
xT4  
7
sZVN  
综合空气管理系统(IAMS: Integrated Air Management System)是确保飞机舒适度最重要的因素之一，其组成部分包括： ]+x;tPo  
}6b=2Z}  
发动机引气系统(Engine bleed air system) )MqF~[k<-  
支持从发动机的低压和高压端口排放高压高温空气。气流通过温度和压力控制设备进行处理，并向下游提供给飞机的主空调系统，机身防冰系统和主机启动系统。该系统包括温度控制阀，压力调节和截止阀，高压阀，过压阀，预冷器热交换器，高压管道，温度传感器，压力传感器，过热/热空气泄漏检测设备以及控制和监视电子单元。 syhTOhOX  
9MA/nybI  
空调系统和机舱空气质量系统(Air conditioning system and cabin air quality system) V~M>K-AL  
支持处理飞机发动机中抽取或“排出”的高压高温空气，该系统的核心由基于空气循环机的空调组件组成，包括热交换器，再热器，冷凝器，水提取器，流量控制阀，传感器或控制器等。这些组件使用空气轴承技术，空气循环机可以是气动驱动的或电动或机械驱动的。 vUh.ev0  
v8p-<N)  
客舱空气分配系统(cabin distribution system) &*iar+vr  
支持将冷却后的空气吹入机舱，并将其引导到适当的区域并在机舱内循环。该系统包括由通风系统、蒸汽循环系统、加热系统和加湿系统等，由压缩机，热交换器，蒸发器，冷凝器，水提取器，电动风扇，阀门，传感器，控制器等组成。 ujsJ;\c  
#!0le:_  
机舱压力控制系统(Cabin pressure control system) OnFx8r:q@%  
气压随着海拔的升高而降低，人体会因此不适。该系统支持控制机舱内部的压力及其变化率，以便为乘客和机组人员的舒适和安全。该系统包括流出和安全阀，控制面板，控制器和软件 :J` *@cDn  
)]~'zOE_  
机翼防冰系统(Airframe anti-icing system) ,":_=Tf.  
该系统承载发动机引气系统提供的热空气，并将其沿机身的冰敏感部分(发动机机舱进气口，机翼和尾翼前缘)吹送。该系统由调压阀，温度传感器，压力传感器，高压管道，过热/热空气泄漏检测装置和控制器组成。 A$vCm  
~Q%C>  
辅助冷却系统(Supplemental cooling system)和液压冷却系统(hydraulic cooling system) (cJb/|?3  
支持以大功率集中式冷却实现食品存储或航空电子热管理。该系统产生的冷却液经过液环分配通过每个需要冷却的地方。连接到该液体回路的热交换器可实现吹向食品的冷空气的功率转换。 =o]V!MW  
液压冷却系统支持冷却飞机上的高压液压通道。 u6h"=l{  
s,>1n0a  
油箱惰化供应(Fuel tank inerting air supply) \hv1"WaJ  
支持提供高压空气，供燃料箱惰化产生氮气。该系统由热交换器，阀门，空气循环机，压缩机等设备组成。 3D70`u  
afOb-G$d=  
航空电子通风系统(Avionics/Electronics cooling) )$V}tr!  
支持用于冷却不同的设备，可延长航空电子设备的使用寿命并提高操作安全性 S*~v9+  
MFO}E!9`q  
综合空气管理系统属于机载设备，通常其软件分配到的研制保证等级(DAL: Development Assurance Level)不低于B级，需要按照DO-178B/C标准的DAL-B级以上的要求进行研发。利勃海尔公司选用了Ansys SCADE作为其安全关键软件的研制工具。 ?<VahDBS+A  
;Q>(%"z};  
WzYy<  
!^BXai/  
3.1 流程设计 [Dd?c,5AD  
图表2是利勃海尔基于Ansys SCADE的综合空气管理系统的控制软件开发V流程。在左侧的开发流，除了文档形式的传统详细设计(LLR)及对应的手工编码外，新增了以SCADE模型为基础的详细设计和相应的认证级代码。右侧验证和确认流程上除软硬件集成测试和系统级测试外，新增了基于SCADE的测试调试环境(STADE：SCADE Test and Debug Environment)。 ;=.VKW%U  
C^I
h"S  
f@lRa>Z(Fm  
:c%vl$  
3.2 基于SCADE模型的开发 3lYM(DT  
流程确定后，根据系统级控制需求设计出图表3所示的控制软件架构图。架构主要包含三个部分:输入、输出和若干个子系统功能。输入和输出可以是多个子系统共用的；子系统根据不同的具体需求设计相应的功能，可包括逻辑功能，动态处理功能，告警功能和执行功能等。 8 St`,Tq)  
fXCx!3m  
%tiFx:F+  
lSU&Yqx  
!/O c)Yk  
5\/h3i"I  
使用Ansys SCADE Suite工具实现控制软件架构图。 w A<JJ_R  
];bB7+  
cU7 c}?J<  
{<%zcNKl^L  
. fq[>zG'&  
U&#1qRm\h  
使用SCADE快速原型工具实现人机仿真界面，支持在PC端与控制软件进行联合仿真。 >J>4g;Y  
+o})Cs`|=A  
=;Gy"F1 dp  
K
IO{6  
Z[:fqvXQ  
3.3 基于SCADE模型的验证 2}:scag  
STADE (STADE：SCADE Test and Debug Environment) 支持基于需求的测试用例设计、在仿真平台和目标机平台的执行和调试，测试结果的收集和处理。测试是包括功能测试和覆盖分析的，STADE复用了SCADE提供的自带工具 (Simulator和MTC) 。 ?'uxYeX6  
4jE
Ph{q  
~$} `R=  
Un\h[m  
利勃海尔在STADE中自定义了测试用例设计规范和转换规则，支持将PC平台仿真无误的测试规程转换为可在目标机平台使用的测试规程。 AU@K5jwDwQ  
0]3%BgZ(a8  
v`8dRVN  
-ZqN~5>j)  
xq1=O  
仿真运行过程通常是命令行形式的，运行完毕的测试结果是支持XML格式的。 @(2DfrC  
*l:5FTp  
vhiP8DQ  
k6-.XW  
?z>Zs
D  
PC平台的仿真无误后，转到目标机平台执行软硬件集成测试。 }wzU<(Rx  
2)(P;[m^o  
z1A[rbe=4w  
软硬件集成测试无误后，最后执行系统级测试。 b489sa  
<EKDP>,~  
>AIkkQT  
.lm^+1}r  
O@St^o*A}  
4、形式化方法辅助生成测试规程 diN5*CF'~  
同绝大部分研制安全关键软件的用户一样，利勃海尔也受困于巨大的测试工作量。即便在引入了基于SCADE的模型化开发验证工具后，依然需要在以下两个部分耗费大量时间。 D(6d#c  
RMU]GCa  
编写测试规程 * Zb-
YA  
当高层需求或模型修改后，修改测试规程 o(5Xj$Z  
=BW>jD  
为了解决这个问题，利勃海尔考虑使用形式化方法来尽可能地自动化这部分工作。 w8i"-SE  
使用形式化的方法定义利勃海尔测试规范语言(LTSL: Liebherr Test Specification Language)，使之半自动化地将测试用例转换为SCADE观察操作符(Observers) Ftu~nh}  
使用形式化方法的方法(模型检查)自动化地生成测试规程 D/C,Q|Ya6  
N9IBw',  
在具体介绍前，先对后面要用到的术语进行介绍。 '#d`K.;_b.  
HLR: High Level Requirement，高层需求，必须被软件实现且必须被测试。通常使用自然语言编写 +4U?*:n  
LLR: Low Level Requirement，低层需求，简言之就是详细设计。当前利勃海尔流程中多数LLR是使用SCADE实现的。HLR和LLR可以是一对一，一对多，多对多的关系。使用SCADE的好处是LLR可直接生成认证级平台无关的C代码供PC或目标机仿真集成测试。 Yy]^_,r  
TC: Test Cases，测试用例，包含输入、期望输出等。TC通常只和HLR相关，用自然语言编写。一个HLR必须被一个或多个TC覆盖。TC和SCADE LLR无关。 `ZL~k  
TP: Test Procedure，测试规程，是TC的可执行地具体实现。TP内包含了TC中定义的输入和期望输出，而且还是可以在PC或目标机上运行的。一个TC必须被一个或多个TP覆盖。 2@WF]*Z  
STS: Software Test Standard，软件测试标准。利勃海尔定义的符合DO-178流程要求的测试标准，指出了在为HLR设计TC和实现TP时需要应用的规则 8d.5D&  
.z7%74p  
根据利勃海尔定义的软件测试标准STS，设计TC必须至少满足以下要求： qXmkeidb&W  
TC的定义应该只参考HLR和HLR变量名称 ]0<T,m Z  
应该记录每个TC的测试目的，即详细说明TC测试覆盖了HLR的哪个方面 e-vL!&;2  
任意两个TC不应该有相同的测试目的 7@"J&><w!  
TC中必须明确说明输入和期望输出 !DFT}eu  
TP的定义应该参考LLR接口名称 xFcJyjo^z  
若干个TC可以在一个TP内依次实现，但应该确保TC在TP中的唯一标识符 )HWf`;VQ  
在TP中，连续TC的期望输出必须不同 $r})j
~c  
STS也推荐了对结构覆盖需要满足的标准 m/l#hp+  
每个TC应该独立地测试各个输入对输出的影响 #:"F-3A0  
对于具有布尔输入的组合逻辑，应该为逻辑真值表的每个可能条目指定一个TC bQc-ryC+.  
对于阈值(threshold)逻辑(例如,范围检查逻辑，确认逻辑等)，应该使用低于阈值输入和高于阈值的输入来检查逻辑输出值。 %|md0  
E?san;Ku  
sE7!U|  
'ms&ty*T  
利勃海尔采用的新测试新流程可减少到TP过程的工作量，尽可能将该过程自动化。该流程关键点如图表11中所示： Dlhb'*@  
步骤5: 设计一套形式化的语言，即利勃海尔测试规范语言(LTSL: Liebherr Test Specification Language)将自然语言设计的TC预先转换为形式化的LTSL LO
{{3No  
步骤6: 使用通用操作符和专门的工具将LTSL转换为SCADE观察器操作符，可用于插桩SCADE模型，供模型检查器调用 T^YdAQeE  
步骤7: 使用模型检查器(Systerel S3)分析插桩后的SCADE模型，驳回观察器输出，生成满足以LTSL表示的测试条件的输入序列。再对序列进行后处理(添加对期望输出的检查等)，形成完整的TP。 }Jkz0JY~  
;QbMVY  
& xOEp  
5、测试规程的自动化生成案例 @#[<5ld  
'&4W@lvyz  
5.1高层需求HLR a&b75.-  
案例选用了第二节介绍的发动机引气系统(Engine bleed air system)的子功能。当前的高层需求HLR为“检测引气是否存在超压”功能的需求1(Req1)。 _IiTB  
9fR`un)f}  
1+6)0 OH{  
!ckm
NE0  
图示的HLR含义为，有三个布尔型输入A,B,C，一个布尔型输出OVPR。  )z#  
OVPR置位逻辑:  当A为true时，OVPR为true，置位逻辑每500毫秒确认一次 Cw"Y=`  
OVPR重置逻辑:  当B为true且A为false时，OVPR重置为false P}B{FIpNG  
或当C为false时，OVPR重置为false, "{-jZdq'  
重置逻辑是立即执行，且优先级高于置位逻辑。 4kZX$ct}  
Nb/W+& y  
5.2测试用例TC :db:|=#T  
根据该引气系统的HLR和第四节中的STS分析出图表13所示的5个TC来覆盖HLR的Req1。其中 W]cJP  
第一行标识出了将被以下TC所覆盖的HLR的标识号Req1 ZaYux-0]kF  
第二行标识出了每个独立的TC的标识号，TC1~TC5 #`R`!4  
第三行标识出了每个TC的测试目的，例如TC1测置位逻辑，TC2和TC4分别测两种重置逻辑，TC3测试维持置位的逻辑，TC5测试重置逻辑的优先级 D.?Rc'yD  
第四行标识出了每个TC各步骤执行所需的最小时间周期，对应着TC包含的一个或多个跟踪片段序列(TSs: Trace Snippets) kd^CZ;O  
第五行标识出了每个TC各步骤执行时的一组输入值 |f+|OZY  
第六行标识出了每个TC各步骤执行后的期望输出值，和相对于TS的输出检查时刻     Tvf%'%h1  
0 =#)-n  
/Zs;dam  
K~Lh'6  
由于图表13中列出的5个TC最终将被整合到一个TP中去，因此TC和TS的顺序就相当重要。精心设计的每个TC既依赖于上个TC执行达到的状态来实现当前的测试目的，又体现了利勃海尔STS中要求的“在TP中，连续TC的期望输出必须不同”。 J WaI[n}  
OL|_@Fv`A  
例如，TC3的步骤1进行了置位，步骤2释放了置位的条件(输入A=False)以测试输出是否维持着置位；TC3必须在尚未置位的情况下开始，因此TC3接着TC2重置后的结果执行较好。而TC2和TC4两个重置的输出False是相同的，所以中间夹个测试“维持置位”功能的TC3(输出为True)就较好。 ^b)8l  
}nNZp  
5*QNE!  
5.3人工手写的测试规程TP (izGF;N+  
Z
%_"-ENT  
b z3&  
M_@%*y\o  
对输入的设置:     SSM::set 变量标识符名称值 /y/O&`X(  
对变量的检查:      Check 变量 期望输出 &wc%mQV  
执行周期设置:      Cycle 周期数 PScq-*^  
注释:                    ;#开头 1I< <`7'  

]A)`I  
^gx`@^su  
=@w,D.5h  
<:=}1t.Z  
5.4 利勃海尔测试规范语言LTSL KICy! "af  
从《基于SCADE模型的形式化方法》一文可知，模型检查可用于生成覆盖分析相关的测试用例，模型检查中常用的系统属性的描述语言是线性时序逻辑语言(LTL: Linear Temporal Logic)。利勃海尔团队也正是利用基于LTL语言定制了利勃海尔测试规范语言(LTSL: Liebherr Test Specification Language)，LTSL语言是为实现测试用例TC到测试规程TP转换而专门设计的形式化语言，它处于图表16流程中的步骤5。 04{*iS95J  
f S-(Kmh  
PYWp2V/  
=?fxPT[1K  
第四节提到的利勃海尔软件测试规范STS中规定LTSL必须满足如下要求： ?CSc5b`eo  
LTSL中必须包含各TC的唯一标识符 ?`R;ZT)U-  
必须以LTSL格式描述每个TC的测试目的 5&V0(LT]C  
必须以LTSL格式描述每个测试用例的输入和期望输出 7!.#:+rg5#  
必须在文件顶部声明HLR和LLR的标识符。因为LTSL更接近TP，所以它还需要LLR的标识符，HLR和LLR都声明便于追踪。 }c/p+Wo  
D{1k{/cF  
#P[d?pY  
KG:CVIW Y  
/~`4a
  
NYopt?Xg  
5.5 SCADE观察操作符的自动生成 os/_ObPiX  
LTSL格式的测试文件准备完毕后，就需要使预先设计好的通用函数和专门工具将LTSL格式文件转换成SCADE文件格式的操作符“Observers”，它处于图表18流程中的步骤6。 R:49Gn:F  
20glz(  
-yKx"Q9F  
*N5cC#5`=  
nk8jXZ"w  
通用函数名称为genSCADEObservers(spec)，输入是LTSL，输出是SCADE操作符observer。转换完毕的observer操作符主要有两类输出：一类是将LTSL内每个Check符号关键字对应的标识符转换为布尔型输出；另一类是名称为Incomplete单独的布尔型输出，该值默认为true，当迭代运行到值为false时，即LTST转换完毕，到达终止状态。 E#'JYz@  
(6##\}L&9  
?V6A:8t,  
Wp!#OY1?
 
实践中利勃海尔的LTLS设计相对简单，并 .. s~OGlPK  
pRS+vV3  

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