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] (內部文檔)