嵌入式系统 | Ansys SCADE在核电项目Connexion中的应用

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项目对核电行业的好处，将通过以下方式为加强法国核电行业生态系统做出了重要贡献：

• 开发保持法国核电行业竞争优势所需的创新

• 增强行业利益相关者的信誉和科学影响力

• 充分利用知识为更新现有核电厂做准备，同时还保持了核电的相关性和吸引力

在核电站中，仪控系统由数百个基础系统(ES: Elementary Systems)组成，以非常高的安全等级控制着数千个远程的执行机构：将超过1万多个的仪控子功能和300个仪控箱的约8000个二进制信号和4000个模拟信号传送到主控室。基础系统由一系列电路和部件组成，它们对核电站的运行起着至关重要的作用。

每个基础系统可分为两个部分：

• 过程(Process)：代表物理基础设施和设备，例如热交换器、阀门、管道等

• 含控制/指令(CC: Control/Command)的实时反应系统(RTS: Real-time reactive system)：该系统不停地与过程(Process)交互，负责保护、控制和管理过程的功能。

每个基础系统都有专门的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流程

为了实现改进的流程，CONNEXION项目需要探索构建一套完整的验证平台，该平台需要选用恰当的商业工具来支撑各个阶段的活动。

针对某个基础系统，平台需要集成控制/指令模型和过程模型，使得系统工程师在开发阶段就能通过控制/指令模型和过程模型进行联合仿真，验证系统的各个方面；需要有与之交互的环境模型，系统运行的期望属性和相关约束，及供工程师操作的人机界面。由于涉及不同模型的集成与多学科联合仿真，平台需要支持FMI(Functional Mock-Up Interface)接口。最后，平台还需要支持信息系统的可追溯性(IST: information system of traceability)，IST活动贯穿于验证和确认活动，不仅保存测试相关的数据，还保存所有活动的历史和相互之间的关系。

图表4: CONNEXION项目的平台

基于平台的构想，选用的工具链如下：

选用CEA基于SysML语言的Papyrus工具实现高层基础系统的模型设计，该模型对应仪控开发改进流程中的功能需求规范阶段

选用基于Modelica语言的Dymola工具实现过程模型的设计

选用Ansys的SCADE Suite工具实现控制/指令模型的设计，该模型对应仪控开发改进流程中的FD和RFD阶段

选用Ansys的SCADE Display工具实现HMI模型的设计

选用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项目选用的工具链

CONNEXION项目使用基于模型的测试(MBT: Model-based testing)方法，可基于被测系统(SUT: system under test)来生成测试用例，其中包含的活动如下：

       步骤1: 基于系统需求开发出模型

       步骤2: 定义测试用例的选择规范

       步骤3: 将测试用例的选择规范转换为可操作的形式化的测试用例

       步骤4: 基于完整定义的模型和测试用例生成测试套件

       步骤5: 执行测试用例

              步骤5-1:将测试用例转换为可执行脚本并送入运行环境

              步骤5-2:比较测试套件/脚本内的期望输出与真实运行输出，判定结果

图表6: CONNEXION项目基于模型的测试流程

传统上，测试策略分为黑盒测试(功能测试)和白盒测试(结构测试)。黑盒测试目的是通过测试设计规范找到程序的错误，黑盒测试中设计的测试用例集不需要分析模型/代码的细节，仅使用设计规范。而白盒测试则相反，侧重于程序的结构。例如，白盒测试中设计的测试用例，能保证每一行代码都至少执行一次。CONNEXION探索将两种测试策略结合起来的方法，使得测试效率将有极大的提升。在继续介绍前，需要对后面使用的术语进行解释。

• 需求requirement：需求是系统必须实现的某功能，而且是可测试的

• 需求覆盖requirement coverage：需求覆盖要求所有需求都包含在功能测试用例集中

• 结构覆盖：通常使用语句覆盖和分支覆盖作为实践的标准。测试用例的设计应该确保语句或分支的覆盖全部达到，体现了测试的充分性

结构覆盖通常有如下几个准则。

• 语句覆盖 SC: statement coverage: 测试用例集必须执行过应用程序中的每个可达到的语句

• 判定覆盖 DC: decision coverage/branch coverage: 测试用例集必须确保每个可达到的判定都至少执行过一次结果为真和结果为假

• 条件变更/判定覆盖 MC/DC: modified condition/decision coverage: 测试用例集对程序中的每个条件强制地改为真和假时，都能独立地影响判定的结果。即在保持其他条件不变的情况下，一个条件被证明可以独立地影响判定的结果。通常，对N个条件最多需要2N个测试用例来覆盖

• 多条件覆盖 MCC: multiple condition coverage: 测试用例集对每个判定的结果都实现了所有可能组合的执行。通常，对N个条件需要多达2N个测试用例来覆盖

需求覆盖和结构覆盖有时是互相独立的，即100%的需求覆盖并不确保100%的结构覆盖，反之亦然。在结构覆盖的各个准则中，MCC需要的工作量最大，强度最高，实现MCC必然实现MC/DC等其他结构覆盖准则。

在进行下一节的详细介绍前，还需要了解几个术语

• SU(structural unit): 模型上的待测分支，覆盖度量单位，与所选的覆盖准则无关

• Reachability check: 模型检查器形式化地验证某SU是否可以被测试执行到

• 开环测试(Open-loop test): 该测试仅考虑本实时系统自身的运行，不考虑与其他实时系统的交互。

• 闭环测试(Closed-loop test): 也称联合执行，本实时系统与整个环境(例如其他实时系统)同时交互运行的测试。

图表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分支记录为潜在不可达的结构覆盖单元，公式为该方法融合了结构覆盖分析的两种结果

• 可达的su分支的结构覆盖都满足了

• 不可达su分支没有未知的，且区分出了是真实不可达SUA，还是潜在不可达SUP(分析超时)。

每次迭代后，(新测试用例集合必包含前测试用例集合)，(前未覆盖单元集合必包含新未覆盖单元集合)，(新达到结构覆盖的数量必大于前达到结构覆盖的数量)。

有可能该方法在初次迭代时就结束，这意味着(测试用例集合)正好满足。另外，只要该方法的左侧循环(步骤8,9,10)执行过，便是实现了本方法用模型检查器改进覆盖分析的初衷。只要该方法的右侧循环(步骤13,14或15,16)执行过，就需要用户进行额外的分析，因为可能存在死代码，甚至是Bug。

通过《基于SCADE模型的形式化方法》我们了解到，模型检查是形式化方法的一种，通常用于搜索一个形式化模型的所有行为，以确定一个指定的属性是否满足。模型检查用于判定系统的形式化模型是否满足基于规约(Specification)的正确属性。这是模型检查的常规用法。

除此之外，可以使用模型检查技术生成覆盖分析相关的测试用例。如果能将测试目标以时序逻辑描述并作为模型检查的属性，就能系统地强制模型检查生成反例，然后将反例改进为覆盖分析相关的测试用例。换言之，需要故意设计一组“缺陷属性”(trap properties)，该缺陷属性声称: 某分支无论如何运行，都不可能被覆盖。模型检查证明该“缺陷属性”为假，就能得到反例，而反例就是可以覆盖该分支的测试用例。

图表8: 模型检查生成测试用例

绝大部分模型检查器在使用时接受三种输入。第一个是被测模型；第二个是根据需求得出的安全属性，即测试目标；第三个是环境描述，即约束条件(图中未标出)。输出结果通常也有三种，属性满足，属性违反(提供反例)和超时(结果不确定)。

图表9: 模型检查的方法

在CONNEXION项目中主要使用GATeL作为模型检查工具，以SCADE构建的控制/指令模型作为被测模型，使用前需要将模型转换为Lustre语言；测试目标为：模型中没有覆盖SU确实不可达；约束条件为一系列布尔表达式，以断言assert形式表述。实践中，GATeL的前两种输入较确定，而约束条件需要逐步精化添加，可将约束条件分为三类：

• 物理约束：只涉及被测模型的输入，物理约束可过滤掉被测模型对应的真实物理系统中不存在的值。例如，水的温度在0~100℃之间

• 初始化约束：只涉及被测模型的输入，初始化约束定义初始周期的输入值，在第一周期执行之后，该约束就不需要了。SCADE/Lustre有专门的时间操作符(pre, init)来表达该约束

• 需求约束: 涉及被测模型的输入和输出。需求约束源于系统的功能需求，定义了输入和输出之间的关系。尽可能将需求约束以布尔表达式或常量形式描述，虽然这并不容易，需要系统设计人员共同的努力。

推荐逐步添加约束条件来执行模型检查。先加物理约束，再加初始化约束，最后再加需求约束。

假定当前某分支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项目中新增模型检查的约束，以精化生成的测试流程

混合验证技术结合了模型检查和仿真两种验证方法。模型检查致力于探索所有可能的状态空间，而仿真仅探索部分的状态空间。混合验证要求多种技术的支持，例如穷举探索状态空间，记录探索的路径，前向/后向路径生成和单步仿真等。

对某待测需求开发的模型进行验证时，需要回答是否可以从初始状态S0开始，找到测试用例运行至目标状态Star。在本文基于模型的测试方法中，未覆盖的SU分支即可认为是目标状态Star。模型检查器在分析该分支时，由于超时没获得确定的结果。

假如模型检查器在超时前能记录所有已经探索的状态空间。例如图标11中已经探索到Sp,Sq,Sl,Sm和Sn共5个状态。就可以再从这5个状态之一(例如Sl)开始进行单步仿真。如何选择恰当的候选状态是混合验证技术的难点，现行的方法是用户自定义的非形式化的方法来预估潜在候选状态与目标状态的距离，可能有些启发式的方法，但较难找到形式化的方法来预估潜在候选状态与目标状态的距离。

图表11: CONNEXION项目中提出的混合验证的思路

SRI是法国核电站的仪控系统中的基础系统。其主要功能是确保其他基础系统(SRI用户)的冷却，SRI通过热交换器与制冷元SEN相连。从图表12中看到：SRI过程包含两个并行工作的热交换器，负责将制冷元SEN的冷水与其他基础系统的热水相混合。三个并行的阀门通过对流量的控制实现热交换，以此调节热交换器出口的水温。水箱用于补偿环路中可能泄漏的水。三个并行的泵确保系统中正常的水循环。

图表12: CONNEXION项目中SRI的简图

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分支的测试用例是相当困难的。

按照4.5节选用了GATeL，Lesar和Kind 2共3款模型检查工具进行了混合验证的试验，结果如下。

图表23: CONNEXION项目应用不同模型检查工具试验混合验证

• GATeL:   通过前面的介绍，GATeL有助于生成改进模型覆盖的测试用例，但GATeL仅提供后向的测试用例生成，而混合验证需要前向/后向的测试用例生成能力。

• Lesar：  探索的状态空间爆炸，结果超时。由于Lesar只能处理布尔型变量，所以不适合处理SRI模型。Lesar在状态空间爆炸时，也没有记录已搜索过的分支结果。所以不适合混合验证。

• Kind 2:  Kind 2依赖商用货架的可满足模块理论(SMT:Satisfiability Modulo Theories)的解算器。而SMT解算器不太适用SRI中控制/指令模型的非线性计算。解决方法是将非线性的表达式转换为以assume-grantee契约形式的抽象表示，再进行分析。改进后的抽象模型可能对安全属性的验证是适合的。

研究团队还试图寻找其他模型检查工具，例如NuSMV，SCADE Design Verifier。但由于经验不足或没有许可证等原因，结果不理想。但依然建议寻找或者开发一款具有如下三种特性的模型检查工具，以实现混合验证技术：

• 支持前向/后向反例生成的测试用例

• 记录超时后的探索过的状态空间

• 仿真后，继续状态空间的搜索

2017年6月，法国电力集团(EDF)发起了名为ConnexITy的倡议，旨在继续将法国核工业的各个合作伙伴联合起来，共同制定如何将重大创新整合到设计和实施核电站的方法中。

同年的11月下旬，ConnexITy的合作方共同成立了核工业数字创新实验室ConnexLab，协同研究开发核电站运行和设计所必需的技术。

Ansys公司主要参与其中两个工作包的研究

• 数字人机建模原型Digital Human Machine Interfaces Prototyping

图表24: Ansys参与ConnexITy项目的数字人机建模原型工作包

• 数字孪生Digital Twin of an Equipment

图表25: Ansys参与ConnexITy项目的数字孪生工作包

CONNEXION项目改进了传统核电站仪控系统的开发流程，将原非可执行的功能设计图(FD)和精化功能图(RFD)以包括SCADE在内的基于模型的方式来开发和验证，使得它们在开发流程早期就能可执行地验证。这对提高安全关键系统的开发效率和安全性是非常有益的。

在基于模型的验证和确认环节，由于涉及不同的模型，最恰当的测试用例必须是基于功能需求的，且可进行闭环测试的。

为了实现测试中的覆盖分析，使用了模型检查技术，帮助生成覆盖分析相关的开环测试用例，并详细介绍了如何逐步添加约束条件，使得自动生成的测试用例序列更适配真实的场景。开环的测试用例转换为闭环的测试用例则需要系统设计师和测试人员的额外工作。

在模型检查结果因状态空间爆炸而超时的情况下，提出了混合验证(融合模型检查和仿真)方法，尽管对混合验证方法的试验结果不够理想，但依然不失为一个生成覆盖分析相关测试用例的好思路，或许选择了更适合的工具就能达到更接近真实场景的结果。

[1] Jean-Christophe BLANCHON. Simulation Driven Engineering applied to nuclear I&C Integrating SCADE with ALICES simulation environment[EB/OL] SUGC 2014 (内部文档)

[2] ALICES Engineering Integration Platform-Example of SCADE integration. [EB/OL] CORYS-Grenoble. INNOVATION IN PARTNERSHIP 2015 (内部文档)

[3] Sun Y, Memmi G, Vignes S. Model-Based Testing Directed by Structural Coverage and Functional Requirements[C]//2016 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). IEEE, 2016: 284-291.

[4] Sun Y, Memmi G, Vignes S. A model-based testing process for enhancing structural coverage in functional testing[M]//Complex Systems Design & Management Asia. Springer, Cham, 2016: 171-180.

[5] Sun Y. Strengthening fonctional validation of critical system by using Model Checking: Application to Instrumentation and Control systems in nuclear power plants[D]. 2017.

[6] Maxime Neyret, Stanislas Couix, Catherine Devic, Franck Noel. ConnexITy French Excellence in Nuclear Innovation within reach of plant reactor operations [EB/OL] (内部文档)