产品
在由Ansys中国系统事业部全新推出的<嵌入式系统>专题内容中，已持续为大家带来Ansys SCADE在航空电传飞控系统、轨交列车控制系统以及航天防卫中的应用做了详细介绍。本期将为大家分享其在核能重工行业的应用案例——核电项目Connexion。本文第一节简要介绍了Connexion项目的内容，第二节描述了改进的仪控系统的开发流程，第三节是Connexion项目根据改进的流程选用的工具链，第四节介绍了项目中基于模型的测试方法，特别是如何使用模型检查技术生成覆盖分析相关的测试用例，第五节以SRI案例介绍具体的应用。第六节是Connexion项目后续演进的介绍。
1Connexion项目简介
2012年法国核电领域的工业方和学术界共同发起了名为CONNEXION(名称源自蓝色字母的缩写COntrôle Commande Nucléaire Numérique pour l'EXport et la rénovatION)的项目。CONNEXION项目的目标是在核电站(Ps: Nuclear Power Plant)的仪表和控制(I&C: Instrumentation & Control，后简称仪控)系统的设计和生产中探索重大创新；为仪控系统的开发和验证创造新的体系架构，而该体系架构可满足法国和国际上核电站的需求。
图表1: CONNEXION项目概览
CONNEXION项目累计获得合作伙伴投资约3600万欧元，其中法国财政部等公共机构投资为1300万欧元，约占36%。项目周期为4年，共有16个合作伙伴。
项目领导是法国电力集团(EDF: Electricite De France)；系统集成商有阿海珐(AREVA)和阿尔斯通(ALSTOM)；学术机构有法国原子能和替代能源委员会(CEA)，法国国家信息与自动化研究所(INRIA)，法国国家科研中心/法国科学院(CNRS/CRAN)，法国卡尚高等师范学校(ENS Cachan)，法国格勒诺布尔理工学院(Grenoble I)，巴黎高科国立高等电信学校(Telecom Paristech)；技术供应商有Esterel(后被Ansys收购)，ALL4TEC，PREDICT，Atos Worldgrid，Rolls-Royce和CORYS。CONNEXION项目与11个子研究项目相关，创造了80个工作岗位，有22个研究生参与。
图表2: 参与CONNEXION项目的16个合作伙伴
CONNEXION项目的范围: 包含构成核电站物理元素的所有资源，这些资源支持自动和人工的管理，检测和控制功能。
CONNEXION项目的三项关键预期成果，可提供：
CONNEXION项目对核电行业的好处，将通过以下方式为加强法国核电行业生态系统做出了重要贡献：
2Connexion项目的流程
在核电站中，仪控系统由数百个基础系统(ES: Elementary Systems)组成，以非常高的安全等级控制着数千个远程的执行机构：将超过1万多个的仪控子功能和300个仪控箱的约8000个二进制信号和4000个模拟信号传送到主控室。基础系统由一系列电路和部件组成，它们对核电站的运行起着至关重要的作用。
每个基础系统可分为两个部分：
每个基础系统都有专门的ESD(Elementary system dossier)文件归档，其中详细包含了基础系统的不同方面：操作、指令/控制，设备等。ESD由功能图(FD)描述，功能图是用符合标准(IEC 61804-1和IEC 61131-3)的非可执行的形式化语言构建的。
传统仪控系统开发的V流程图(图表3)中主要涉及共七个步骤(1,2,4,7,8,9,10)。其中左侧的(1,2,3,7)为开发流程中的设计与实现，右侧的(8,9,10)为测试流程中的验证与确认。左侧的开发流程通常是针对单个基础系统的，而其右侧的测试流程则需要将基础系统集成到虚拟平台才能测试。
该流程先从左侧的功能需求规范(specification of functional requirements)开始，细化为详细功能设计(FD: detailed functional specification)，再逐步细化为精化功能图(RFD: Refined Functional Diagram)，再实现为可执行程序。验证和确认(V&V: Verification and Validation)活动都是基于可执行程序的，先基于RFD验证某仪控的ES，再基于FD验证集成了其他ES的仪控系统，最终所有经过验证的ES集成到一个平台后，再对其功能进行确认。
而CONNEXION项目对传统仪控开发的V流程进行了改造，在左侧开发流的 RD和RFD阶段就引入了对功能需求的验证。这样原V流程就新包含了两个子流程：1,2,3和1,2,4,5,6。由于传统的FD和RFD都不是可执行程序，所以其验证活动都是人工评审。只有将FD和RFD都以等价的可执行的形式化语言来描述，才能自动化地进行功能测试。CONNEXION项目为此提供了满足该要求的完整工具链。
值得一提的是，新流程也是符合IEC 60880标准的，因为标准中鼓励使用自动化的测试工具。又因为新流程中使用的形式化工具是作为测试用例的生成器，而不是形式化证明的工具；即该工具只是对测试用例人工编写活动的辅助，而不是替代。因此新流程中集成的工具并不意味着必须对它进行鉴定。
CONNEXION项目使得传统以文档为基础的系统工程转变为INCOSE提倡的以模型为基础的系统工程。而这其中的关键就是在类似工业网络物理系统(Industrial Cyber-Physical System)的传统V流程中新引入了两个切实可行的子流程，从而实现了V流程中早期的验证和确认。
图表3: CONNEXION项目改进的仪控系统V流程
3Connexion项目的工具链
为了实现改进的流程，CONNEXION项目需要探索构建一套完整的验证平台，该平台需要选用恰当的商业工具来支撑各个阶段的活动。
针对某个基础系统，平台需要集成控制/指令模型和过程模型，使得系统工程师在开发阶段就能通过控制/指令模型和过程模型进行联合仿真，验证系统的各个方面；需要有与之交互的环境模型，系统运行的期望属性和相关约束，及供工程师操作的人机界面。由于涉及不同模型的集成与多学科联合仿真，平台需要支持FMI(Functional Mock-Up Interface)接口。最后，平台还需要支持信息系统的可追溯性(IST: information system of traceability)，IST活动贯穿于验证和确认活动，不仅保存测试相关的数据，还保存所有活动的历史和相互之间的关系。
图表4: CONNEXION项目的平台
基于平台的构想，选用的工具链如下：
3.1 选用的开发工具
选用CEA基于SysML语言的Papyrus工具实现高层基础系统的模型设计，该模型对应仪控开发改进流程中的功能需求规范阶段
选用基于Modelica语言的Dymola工具实现过程模型的设计
选用Ansys的SCADE Suite工具实现控制/指令模型的设计，该模型对应仪控开发改进流程中的FD和RFD阶段
选用Ansys的SCADE Display工具实现HMI模型的设计
3.2 选用的验证工具
选用All4Tech的MaTeLo做基于模型的测试生成工具。该工具支持从用户角度，使用马尔科夫链通过统计或确定性方法等生成基于功能需求规范的测试用例，生成的测试用例可用于闭环测试。
选用CEA的INTERVAL自动生成可执行程序的测试用例。该工具的输入是xLia格式的系统模型，xLia格式的系统模型是由Papyrus的SysML半自动化地转换而来。
选用CEA的GATeL工具实现模型检查，该工具是基于同步语言Lustre的。GATeL可验证系统可达状态的属性，或某属性是不变的。另外，针对扩展的Lustre语言所描述的测试目标，GATeL支持自动生成满足该目标的测试用例。
选用Ansys的SCADE QTE实现基于模型的验证。该工具支持获取模型级的功能测试结果和覆盖分析结果。
选用CEA的ARTiMon实现平台级的功能测试。由于MaTeLo生成的测试用例不含期望输出，ARTiMon支持插入相关观察信息，使得在平台级闭环仿真时，将执行结果不一致情况保存下来。
选用CORYS的ALICES实现平台的闭环仿真。由于控制/指令模型和过程模型是基于不同语言的，ALICES支持通过FMI/FMU实现两种模型的交互和数据同步。
图表5: CONNEXION项目选用的工具链
4基于模型的测试
CONNEXION项目使用基于模型的测试(MBT: Model-based testing)方法，可基于被测系统(SUT: system under test)来生成测试用例，其中包含的活动如下：
步骤1: 基于系统需求开发出模型
步骤2: 定义测试用例的选择规范
步骤3: 将测试用例的选择规范转换为可操作的形式化的测试用例
步骤4: 基于完整定义的模型和测试用例生成测试套件
步骤5: 执行测试用例
步骤5-1:将测试用例转换为可执行脚本并送入运行环境
步骤5-2:比较测试套件/脚本内的期望输出与真实运行输出，判定结果
图表6: CONNEXION项目基于模型的测试流程
4.1 选用的测试策略及相关术语
传统上，测试策略分为黑盒测试(功能测试)和白盒测试(结构测试)。黑盒测试目的是通过测试设计规范找到程序的错误，黑盒测试中设计的测试用例集不需要分析模型/代码的细节，仅使用设计规范。而白盒测试则相反，侧重于程序的结构。例如，白盒测试中设计的测试用例，能保证每一行代码都至少执行一次。CONNEXION探索将两种测试策略结合起来的方法，使得测试效率将有极大的提升。在继续介绍前，需要对后面使用的术语进行解释。
结构覆盖通常有如下几个准则。
需求覆盖和结构覆盖有时是互相独立的，即100%的需求覆盖并不确保100%的结构覆盖，反之亦然。在结构覆盖的各个准则中，MCC需要的工作量最大，强度最高，实现MCC必然实现MC/DC等其他结构覆盖准则。
在进行下一节的详细介绍前，还需要了解几个术语
4.2 基于模型的测试方法
图表7: CONNEXION项目中自动化生成模型覆盖相关测试用例的方法
如图所示，共有16个步骤。
步骤1：根据功能需求中的测试目标，使用基于模型的功能测试用例生成工具MaTeLo生成功能测试 用例集(TS: test set)
步骤2：在配置完毕的平台环境(ALICES)中，对系统模型进行闭环测试
步骤3：由覆盖分析工具(SCADE QTE)获取结构覆盖的结果。当恰好覆盖准则满足，即全部覆盖时，则验证工作结束
步骤4：定义SUU,是所有未实现结构覆盖单元的集合
定义SUA,是所有真实不可达的结构覆盖单元的集合
定义SUP,是所有潜在不可达的结构覆盖单元的集合，即仅由于操作方法等原因而不可达。
将步骤3中未实现结构覆盖单元保存到SUU，并初始化SUA和SUP变量为空
步骤5：迭代计算，公式含义: 所有未实现结构覆盖的单元都区分出到底是真实不可达的，还是潜在不可达的。初次迭代执行到此时SUU不为空，而SUA和SUP为空。当某次迭代执行到SUU为空时，即则验证工作结束。
步骤6：从SUU中取出某个未结构覆盖的单元su分支，
步骤7：使用模型检查器验证su分支的可达性
如果su分支确实不可达，执行步骤13，步骤14和步骤5，再继续迭代执行
如果su分支是可达的，执行步骤8，步骤9，步骤10和步骤2，再继续迭代执行
如果模型检查结果是超时(TO: TIME OUT)，执行步骤11
步骤8：模型检查器自动生成了对应的开环测试用例
步骤9：根据开环测试用例，构建新的闭环功能测试用例ntc (new test case)
该工作需要系统设计师和测试人员的协作，根据高层功能需求确认ntc是真实有效的。该测试用例不仅对当前su分支的结构覆盖有效，还可能对其他su分支的结构覆盖也有效
步骤10：将新增的ntc添加到步骤1生成的功能测试用例集中，公式为
步骤11：执行包含“模型检查和仿真”技术的混合仿真
步骤12：混合仿真后，再次检查su分支的可达性
如果su分支是可达的，执行步骤8，步骤9，步骤10和步骤2，再继续迭代执行
如果模型检查结果再次是超时(TO)，执行步骤15,步骤16和步骤5，再继续迭代执行
步骤13：发送“不可达”的警告信息给用户
步骤14：将su分支记录为真实不可达的结构覆盖单元，公式为
步骤15：发送“放弃”的警告信息给用户
步骤16：将su分支记录为潜在不可达的结构覆盖单元，公式为该方法融合了结构覆盖分析的两种结果
每次迭代后，(新测试用例集合必包含前测试用例集合)，(前未覆盖单元集合必包含新未覆盖单元集合)，(新达到结构覆盖的数量必大于前达到结构覆盖的数量)。
有可能该方法在初次迭代时就结束，这意味着(测试用例集合)正好满足。另外，只要该方法的左侧循环(步骤8,9,10)执行过，便是实现了本方法用模型检查器改进覆盖分析的初衷。只要该方法的右侧循环(步骤13,14或15,16)执行过，就需要用户进行额外的分析，因为可能存在死代码，甚至是Bug。
4.3 使用模型检查技术生成覆盖分析相关的测试用例
通过《基于SCADE模型的形式化方法》我们了解到，模型检查是形式化方法的一种，通常用于搜索一个形式化模型的所有行为，以确定一个指定的属性是否满足。模型检查用于判定系统的形式化模型是否满足基于规约(Specification)的正确属性。这是模型检查的常规用法。
除此之外，可以使用模型检查技术生成覆盖分析相关的测试用例。如果能将测试目标以时序逻辑描述并作为模型检查的属性，就能系统地强制模型检查生成反例，然后将反例改进为覆盖分析相关的测试用例。换言之，需要故意设计一组“缺陷属性”(trap properties)，该缺陷属性声称: 某分支无论如何运行，都不可能被覆盖。模型检查证明该“缺陷属性”为假，就能得到反例，而反例就是可以覆盖该分支的测试用例。
图表8: 模型检查生成测试用例
绝大部分模型检查器在使用时接受三种输入。第一个是被测模型；第二个是根据需求得出的安全属性，即测试目标；第三个是环境描述，即约束条件(图中未标出)。输出结果通常也有三种，属性满足，属性违反(提供反例)和超时(结果不确定)。
图表9: 模型检查的方法
在CONNEXION项目中主要使用GATeL作为模型检查工具，以SCADE构建的控制/指令模型作为被测模型，使用前需要将模型转换为Lustre语言；测试目标为：模型中没有覆盖SU确实不可达；约束条件为一系列布尔表达式，以断言assert形式表述。实践中，GATeL的前两种输入较确定，而约束条件需要逐步精化添加，可将约束条件分为三类：
推荐逐步添加约束条件来执行模型检查。先加物理约束，再加初始化约束，最后再加需求约束。
4.4 GATeL约束的逐步精化
假定当前某分支SU未覆盖，模型检查器GATeL逐步定义约束条件来验证该SU是否可达。先加第一个约束条件C1，GATeL运行后可能产生三种输出：
(1)：SU是可达的(R)
(2)：SU是不可达的(NR)。这种情况下不需要再额外添加约束，SU可记录为不可达分支。
(3)：结果不确定，GATeL运行超时(TO: TIME OUT)
对输出(1)或(3)，需要逐步增加新的约束条件C2，再通过GATeL验证SU的可达性。此时输出为：
(1.1)：SU依然是可达的(R)。此时GATeL又生成了一组测试用例序列，而SU是在该测试用例序列执行的最后一个周期才覆盖。该测试用例序列就是逐步满足约束C1∧C2∧﹍Cn的更接近真实场景和物理现实的开环测试用例。也有助于后期覆盖SU的闭环测试用例的构建。
(1.2)：SU变为不可达的(NR)。这意味着之前的结果R(1)可能是不真实的，需要更多分析。原因可能如下：1.SU可能就是不可达的，2.约束条件不正确，3.约束条件违反了模型对应的需求
(1.3)：结果不确定，GATeL运行超时(TO)。通常添加约束意味着减少GATeL需要探索的状态空间。对于这种情况，一种可能的解释是(1)中先前的测试用例序列被新添加的约束消除了，GATeL在限定的时间内找不到新的测试用例序列来覆盖SU。
(3.1)：SU是可达的(R)。随着约束的增多，GATeL生成了覆盖SU的真实测试用例序列。
(3.2)：SU是不可达的(NR)。可以更有信心地假设SU就是不可达的。
(3.3)：结果不确定，GATeL运行超时(TO)。需要引入混合验证(hybrid verification)技术来分析。
图表10: CONNEXION项目中新增模型检查的约束，以精化生成的测试流程
4.5 混合验证技术的探索
混合验证技术结合了模型检查和仿真两种验证方法。模型检查致力于探索所有可能的状态空间，而仿真仅探索部分的状态空间。混合验证要求多种技术的支持，例如穷举探索状态空间，记录探索的路径，前向/后向路径生成和单步仿真等。
对某待测需求开发的模型进行验证时，需要回答是否可以从初始状态S0开始，找到测试用例运行至目标状态Star。在本文基于模型的测试方法中，未覆盖的SU分支即可认为是目标状态Star。模型检查器在分析该分支时，由于超时没获得确定的结果。
假如模型检查器在超时前能记录所有已经探索的状态空间。例如图标11中已经探索到Sp,Sq,Sl,Sm和Sn共5个状态。就可以再从这5个状态之一(例如Sl)开始进行单步仿真。如何选择恰当的候选状态是混合验证技术的难点，现行的方法是用户自定义的非形式化的方法来预估潜在候选状态与目标状态的距离，可能有些启发式的方法，但较难找到形式化的方法来预估潜在候选状态与目标状态的距离。
图表11: CONNEXION项目中提出的混合验证的思路
5Connexion项目SRI案例
SRI是法国核电站的仪控系统中的基础系统。其主要功能是确保其他基础系统(SRI用户)的冷却，SRI通过热交换器与制冷元SEN相连。从图表12中看到：SRI过程包含两个并行工作的热交换器，负责将制冷元SEN的冷水与其他基础系统的热水相混合。三个并行的阀门通过对流量的控制实现热交换，以此调节热交换器出口的水温。水箱用于补偿环路中可能泄漏的水。三个并行的泵确保系统中正常的水循环。
图表12: CONNEXION项目中SRI的简图
SRI的控制/指令功能为
5.2 SRI案例的建模与测试
CONNEXION项目的合作方之一阿海珐(AREVA)参与了这方面的工作。SRI的控制/指令功能是用SCADE Suite建模实现的。
图表13: CONNEXION项目中SCADE实现的SRI的某控制/指令模型
根据功能需求，使用MaTeLo生成了含10个用例的测试集(即4.2节步骤1)，并在ALICES平台上进行闭环仿真(即4.2节步骤2)。将该阶段使用的含测试用例脚本，结合SCADE QTE应用到构建控制/指令模型的单个操作符上，以获取MC/DC覆盖分析结果(即4.2节步骤3)。
图表14: CONNEXION项目中某SRI的控制/指令模型的覆盖分析测试方法
使用SCADE QTE获取的覆盖分析结果如图。绿色表示完全覆盖，黄色表示部分覆盖，红色表示未覆盖。控制/指令模型是由一系列SCADE模型组件的，其顶层操作符名称为“ControlCommande”(图表15中红框包围)，当前覆盖分析结果约为50%。
图表15: CONNEXION项目中某SRI的控制/指令模型的覆盖分析结果
由于未达到完全覆盖，可使用GATeL对未覆盖的SU分支进行可达性分析(即4.2节步骤6)。考虑选用最底层的操作符进行验证，因为它不包含其他的操作符。选用它进行可达性分析后获取的测试用例不仅能覆盖当前SU分支，还可能覆盖其他高层的未覆盖SU分支。如图示，选用了含三个层级的最底层操作符，该操作符有两个布尔型输入i1和i2，和一个and逻辑操作符，其and为true的分支未覆盖。
图表16: CONNEXION项目内选中某未覆盖SU进行测试
按照4.4节的方法，依次添加4.3节描述的三类约束后，使用GATeL对该操作符进行可达性分析。
首先构建物理约束C1共含3项内容
1. 水温在0~100℃之间
图表17: CONNEXION项目内GATeL定义的水温约束
2. 水箱的水位在0~最高位置之间
图表18: CONNEXION项目内GATeL定义的水箱的水位约束
3. 泵的运行态和缺省态两个布尔值不可能同时为真(泵的运行态为真，意味着水箱不处于缺省态)
图表19: CONNEXION项目内GATeL定义的泵约束
先使用约束C1进行模型检查后，生成包含三个周期的测试用例序列将SU分支覆盖。
考察SU分支的详细覆盖结果(图表20)，S0是原闭环测试积累的测试用例，未覆盖All True列(×号是覆盖)。localVar2是GATeL模型检查生成的测试用例，覆盖了All True列。
图表20: CONNEXION项目某SU分支的新覆盖结果
考察顶层操作符ControlCommande的详细覆盖结果(图表21)，S0测试用例的覆盖率为63/121,localVar2测试用例的覆盖率为85/121，TS0+localVar2两套测试用例的覆盖率为101/121，覆盖率由50%提升到了80%。这意味着其他高层未覆盖的分支也由当前模型检查新生成的测试用例覆盖了。
图表21: CONNEXION项目某顶层操作符分支的新覆盖结果
在物理约束C1的基础上添加初始化约束C2，C2假定系统的两个热交换器初始化为工作正常。
图表22: CONNEXION项目内GATeL定义的初始化约束
GATeL在C1∧C2的约束基础上进行的模型检查结果为超时。通过将GATeL配置的默认测试用例序列长度由20改为30后，GATeL的再次模型检查获得了长度为23周期的测试用例序列。此次GATeL计算耗时6391秒，消耗272309千字节。这证明了通过精化约束条件，确实可以使得模型检查生成的测试用例更加逼近真实场景。而长达23周期的测试序列，也说明靠人工设计可覆盖该SU分支的测试用例是相当困难的。
5.3 SRI案例对混合验证的试验
按照4.5节选用了GATeL，Lesar和Kind 2共3款模型检查工具进行了混合验证的试验，结果如下。
图表23: CONNEXION项目应用不同模型检查工具试验混合验证
研究团队还试图寻找其他模型检查工具，例如NuSMV，SCADE Design Verifier。但由于经验不足或没有许可证等原因，结果不理想。但依然建议寻找或者开发一款具有如下三种特性的模型检查工具，以实现混合验证技术：
6Connexion项目的后续演进
2017年6月，法国电力集团(EDF)发起了名为ConnexITy的倡议，旨在继续将法国核工业的各个合作伙伴联合起来，共同制定如何将重大创新整合到设计和实施核电站的方法中。
同年的11月下旬，ConnexITy的合作方共同成立了核工业数字创新实验室ConnexLab，协同研究开发核电站运行和设计所必需的技术。
Ansys公司主要参与其中两个工作包的研究
图表24: Ansys参与ConnexITy项目的数字人机建模原型工作包
图表25: Ansys参与ConnexITy项目的数字孪生工作包
7小结
CONNEXION项目改进了传统核电站仪控系统的开发流程，将原非可执行的功能设计图(FD)和精化功能图(RFD)以包括SCADE在内的基于模型的方式来开发和验证，使得它们在开发流程早期就能可执行地验证。这对提高安全关键系统的开发效率和安全性是非常有益的。
在基于模型的验证和确认环节，由于涉及不同的模型，最恰当的测试用例必须是基于功能需求的，且可进行闭环测试的。
为了实现测试中的覆盖分析，使用了模型检查技术，帮助生成覆盖分析相关的开环测试用例，并详细介绍了如何逐步添加约束条件，使得自动生成的测试用例序列更适配真实的场景。开环的测试用例转换为闭环的测试用例则需要系统设计师和测试人员的额外工作。
在模型检查结果因状态空间爆炸而超时的情况下，提出了混合验证(融合模型检查和仿真)方法，尽管对混合验证方法的试验结果不够理想，但依然不失为一个生成覆盖分析相关测试用例的好思路，或许选择了更适合的工具就能达到更接近真实场景的结果。
免责声明：本文系网络转载或改编，未找到原创作者，版权归原作者所有。如涉及版权，请联系删
155-2731-8020
