基于合約的SCADE測試工具設(shè)計與實現(xiàn)

劉小同+熊夢+陽小華+劉杰

摘要：反應(yīng)堆保護(hù)系統(tǒng)是核電廠中最重要的安全系統(tǒng)，對保證核電設(shè)備、工作人員以及周邊環(huán)境的安全有著至關(guān)重要的作用。由于反應(yīng)堆保護(hù)系統(tǒng)所需要的高安全性，因～LSCADE平臺開發(fā)的壓水堆反應(yīng)堆保護(hù)系統(tǒng)（以下簡稱SCADE系統(tǒng)）是近年來重要的研究方向。但是SCADE平臺的開發(fā)過程基本以圖形方式展現(xiàn)，設(shè)計與驗證工作也都在SCADE系統(tǒng)內(nèi)部完成，缺少對內(nèi)部的本質(zhì)特征的說明。因此需要一種方法來對SCADE系統(tǒng)的內(nèi)部結(jié)構(gòu)進(jìn)行解釋，并根據(jù)此對SCADE系統(tǒng)進(jìn)行后期的驗證工作提供理論支持，確保對SCADE系統(tǒng)的驗證工作是有效的。筆者由此提出了基于合約的SCADE測試?yán)碚摚⒏鶕?jù)此理論設(shè)計并開發(fā)了基于合約的SCADE自動測試平臺，用于為SCADE系統(tǒng)的驗證工作提供充分的測試用例并進(jìn)行相關(guān)測試工作。

關(guān)鍵詞：反應(yīng)堆保護(hù)系統(tǒng)；SCADE系統(tǒng)；基于合約的測試平臺

1概述

隨著核電產(chǎn)業(yè)的不斷發(fā)展，核電廠核反應(yīng)堆的安全問題已經(jīng)引起業(yè)內(nèi)人士的廣泛關(guān)注。反應(yīng)堆保護(hù)系統(tǒng)（ReactorProtection System，RPS）作為在核反應(yīng)堆投入使用后對反應(yīng)堆進(jìn)行保護(hù)的安全系統(tǒng)，也在不斷的研發(fā)。通常情況下，反應(yīng)堆保護(hù)系統(tǒng)通過SCADE平臺進(jìn)行開發(fā)。SCADE是一個基于組件式的嵌入式控制系統(tǒng)開發(fā)平臺，設(shè)計人員根據(jù)設(shè)計需求，將已存在或已開發(fā)好的基礎(chǔ)模塊進(jìn)行組裝，最終形成一個完整的系統(tǒng)，設(shè)計好的系統(tǒng)通過SCADE平臺生成最終的c語言代碼，用于寫人到硬件中作為最終產(chǎn)品使用。

SCADE采用圖形化的開發(fā)過程可以提高開發(fā)者對整個系統(tǒng)的觀察深度和控制復(fù)雜度的能力，提高生產(chǎn)率，有效地避免了代碼內(nèi)部的編碼錯誤。但是整個開發(fā)過程都是以圖形的方式表現(xiàn)，設(shè)計和驗證工作都在SCADE系統(tǒng)內(nèi)完成。對于SCADE模型本身性質(zhì)特征缺少說明。對于SCADE軟件系統(tǒng)燒錄到芯片后的檢驗缺乏必要的數(shù)據(jù)和信息支持。因此需要針對SCADE模型生成相應(yīng)的抽象模型說明系統(tǒng)的性質(zhì)。其作用可以驗證模型是否滿足需求，以及提供足夠的信息檢驗后期的硬件實現(xiàn)是否滿足系統(tǒng)要求。

而目前的SCADE的模型來源于設(shè)計方案圖紙，缺乏對系統(tǒng)整體性質(zhì)的設(shè)計說明。而Bertrand Meyer提出的軟件合約理論，可以比較精確的描述出使用組件的約束以及使用后構(gòu)件預(yù)期的正確狀態(tài)。如果組件違背約束，將引發(fā)失效。隨著組件的組織結(jié)構(gòu)，向外擴展，最終影響系統(tǒng)的整體性能。組件的失效會通過組件之間的接口影響到其他組件。既有可能是某些或某類失效傳播到下一構(gòu)件，也可能在失效傳播的過程中，轉(zhuǎn)換為其他類型的失效模式。最終將導(dǎo)致整個系統(tǒng)的事故。

將SCADE組件的約束模型抽象為合約，可以作為DI&C軟件系統(tǒng)邏輯的正確表示方法，用于對系統(tǒng)進(jìn)行可靠性與安全性檢驗。因此，我們針對基于SCADE開發(fā)的DI&C系統(tǒng)開發(fā)了基于合約的SCADE測試工具，為系統(tǒng)生成系統(tǒng)合約，并生成測試用例、測試腳本和期望輸出，對系統(tǒng)的正確性進(jìn)行充分驗證。

2基于SCADE模塊的合約測試?yán)碚?/p>

軟件合約理論是Bertrand Meyer等人為提高程序設(shè)計質(zhì)量而提出的。它把軟件模塊之間的交互規(guī)則定義為合約，通過合約來明確模塊調(diào)用方與實現(xiàn)方之間的職責(zé)和權(quán)利。

以SCADE組件形成的約束模型（合約）作為基礎(chǔ)，對系統(tǒng)進(jìn)行分析后設(shè)計出驗證系統(tǒng)所需的測試用例以及期望輸出，可以有效驗證SCADE搭建的系統(tǒng)。因此，根據(jù)合約理論設(shè)計相應(yīng)的方法對SCADE搭建的系統(tǒng)進(jìn)行驗證，可以提高系統(tǒng)的可靠性與安全性，防止系統(tǒng)出現(xiàn)嚴(yán)重的錯誤，并減少人工驗證的工作量。

2.1 SCADE模塊開發(fā)

在SCADE平臺上進(jìn)行開發(fā)時，首先根據(jù)不同的基礎(chǔ)功能開發(fā)出相應(yīng)的基礎(chǔ)模塊，然后根據(jù)系統(tǒng)設(shè)計用基礎(chǔ)模塊搭建成完整的系統(tǒng)。

DI&C軟件系統(tǒng)基于SCADE基礎(chǔ)模塊搭建而成，其合約的生成方法需要2個步驟，首先通過合約抽取技術(shù)從基礎(chǔ)組件中抽取基礎(chǔ)組件合約，然后分析構(gòu)建系統(tǒng)的模塊結(jié)構(gòu)特征，依據(jù)系統(tǒng)結(jié)構(gòu)特征采用合約組合技術(shù)生成系統(tǒng)合約。

DI&C系統(tǒng)由各個基礎(chǔ)模塊組合而成，簡單的復(fù)合模塊基本分為串聯(lián)和并聯(lián)兩種情況，復(fù)雜的復(fù)合模塊以及系統(tǒng)組合均由基本模塊進(jìn)行復(fù)雜的串并聯(lián)后得到。所以掌握基礎(chǔ)模塊簡單的串聯(lián)和并聯(lián)組合方法即可分析出DI&C軟件的系統(tǒng)合約。

2.2 SCADE模塊合約

SCADE搭建的系統(tǒng)中，基礎(chǔ)模塊包括輸入、輸出、參數(shù)等模塊接口信息，以及模塊的約束規(guī)則。根據(jù)接口信息和約束規(guī)則，我們將SCADE模塊抽象為合約，形成邏輯模塊，用于組合成系統(tǒng)合約。

每個模塊都具有一個以上（含1）的輸入和輸出與零個以上（含0）的參數(shù)，它們由值（value）和狀態(tài)（state）兩部分組成，“值”分為模擬量（analog）和二進(jìn)制量（binary），“狀態(tài)”僅有故障（FAULT）或無故障（NO_FAULT）兩種情況。模塊約束規(guī)則分為參數(shù)規(guī)則（Rule_para）、值規(guī)則（Rule_value）和狀態(tài)規(guī)則（Rule_state），他們都包含一個以上（含1）的子合約。這些接口與約束規(guī)則共同構(gòu)成了基礎(chǔ)模塊的合約。

2.3 SCADE系統(tǒng)合約生成

在DI&C軟件中，系統(tǒng)由基礎(chǔ)模塊搭建而成。將基礎(chǔ)模塊按照一定的組織結(jié)構(gòu)進(jìn)行組合，實現(xiàn)系統(tǒng)設(shè)計的功能。在外界環(huán)境確定的情況下，組合結(jié)構(gòu)決定了系統(tǒng)功能，即組合結(jié)構(gòu)決定系統(tǒng)的輸入、輸出、參數(shù)以及各個部分之間關(guān)系，因此根據(jù)基礎(chǔ)模塊的合約進(jìn)行組合與分析，最終形成完整的系統(tǒng)合約，具有很高的可行性。

我們將DI&C系統(tǒng)中，基礎(chǔ)模塊的組合方式分為串聯(lián)組合和并聯(lián)組合，系統(tǒng)組合由大量模塊經(jīng)過設(shè)計好的串聯(lián)并聯(lián)得到。

在串聯(lián)組合中，兩模塊前后鏈接形成新的復(fù)合模塊。1）模塊接口中，上一模塊輸出作為下一模塊輸入。所以，串聯(lián)模塊輸入為上一模塊輸入，串聯(lián)模塊輸出為下一模塊輸出。因模塊參數(shù)基本相互無影響，故串聯(lián)模塊參數(shù)為兩模塊參數(shù)并集。2）模塊合約中，復(fù)合模塊合約由串聯(lián)模塊合約合并而成，將兩模塊合約集相乘得到笛卡爾集，將其中上一模塊的輸入與下一模塊輸出以臨時量進(jìn)行連接后，即得到總的合約。然后對合約進(jìn)行進(jìn)一步的簡化合并，去掉臨時量，得到串聯(lián)模塊總的合約。

并聯(lián)組合中，兩模塊并聯(lián)形成新的復(fù)合模塊。1）模塊接口上，兩模塊可能共用全部輸入，也可能共用部分輸入，也可能各自有不同的輸入，所以并聯(lián)模塊的輸入為兩模塊輸入的并集，輸出為兩模塊輸出的并集。同時，并聯(lián)模塊間的參數(shù)相互無影響，所以并聯(lián)模塊參數(shù)為兩模塊參數(shù)的并集。21模塊合約中，由于并聯(lián)模塊之間運行互不影響，所以并聯(lián)模塊的合約為兩個基礎(chǔ)模塊合約集的并集。

根據(jù)我們定義的模塊合約，將系統(tǒng)拆分為基礎(chǔ)模塊并得到基礎(chǔ)模塊的組合方式。再根據(jù)基礎(chǔ)模塊的組合方式將基礎(chǔ)模塊合約組合為整個系統(tǒng)的合約。分別取每個模塊的某個子合約公式進(jìn)行排列組合，即可得到系統(tǒng)所有的狀態(tài)，然后對這些狀態(tài)進(jìn)行篩選，去掉無用或不可能存在的狀態(tài)，即可得到所有可能存在的狀態(tài)，然后根據(jù)每個狀態(tài)的約束條件，設(shè)計符合條件的測試用例，由此得到整個系統(tǒng)的測試用例，對系統(tǒng)進(jìn)行充分的測試。

3基于合約的SCADE模型自動測試工具結(jié)構(gòu)設(shè)計基于合約的SCADE模型自動測試工具的設(shè)計主要分為基礎(chǔ)模塊合約管理和基于合約的SCADE測試兩大模塊?；诤霞s的SCADE測試分為導(dǎo)入待測系統(tǒng)、拆分待測系統(tǒng)、抽取基礎(chǔ)模塊、組合基礎(chǔ)模塊、生成系統(tǒng)合約、生成測試用例、生成測試腳本、生成期望輸出等八個部分。

基礎(chǔ)模塊合約管理部分主要包括基礎(chǔ)模塊類和管理類，負(fù)責(zé)對基礎(chǔ)模塊合約進(jìn)行管理，包括基礎(chǔ)模塊的添加、刪除、編輯和查找等功能。

基于合約的SCADE測試部分主要包含待測系統(tǒng)類與針對待測系統(tǒng)進(jìn)行操作的各個操作類。負(fù)責(zé)對待測系統(tǒng)進(jìn)行解析、拆分、合成合約、生成測試用例、生成測試腳本、生成期望輸出等操作。

1）導(dǎo)入待測系統(tǒng)

通過分析SCADE平臺搭建的系統(tǒng)的文件存儲方式，將整個系統(tǒng)所有文件導(dǎo)入到軟件中，并通過解析得出所導(dǎo)入的系統(tǒng)的信息；

解析系統(tǒng)信息同樣通過解析系統(tǒng)項目文件中的.xscade文件，解析方式與基礎(chǔ)模塊解析相同，因為系統(tǒng)項目由不同的基礎(chǔ)模塊搭建而成，所以系統(tǒng)項目的.xscade文件中，Data標(biāo)簽下的Equation標(biāo)簽中，CallExpression標(biāo)簽內(nèi)即為引用的基礎(chǔ)模塊的信息，OpCall中的name值為引用操作的實例名，operator中的OperatorRef標(biāo)簽中的那么值為引用的基礎(chǔ)模塊的名稱。

2）拆分待測系統(tǒng)

根據(jù)解析得到的系統(tǒng)信息，將系統(tǒng)拆分得到一個個的基礎(chǔ)模塊；

3）抽取基礎(chǔ)模塊

整理拆分得到的基礎(chǔ)模塊，在軟件保存的基礎(chǔ)模塊庫中查找系統(tǒng)所需的基礎(chǔ)模塊的合約等信息。如果找不到所需模塊，則給出相應(yīng)提示；

4）組合基礎(chǔ)模塊

通過對系統(tǒng)的解析，得出系統(tǒng)中基礎(chǔ)模塊的組合方法；系統(tǒng)中基礎(chǔ)模塊的組合方法由基礎(chǔ)的串聯(lián)、并聯(lián)組合混合而成，由此連接組合為整個復(fù)雜的系統(tǒng)。

5）生成系統(tǒng)合約

根據(jù)組合基礎(chǔ)模塊中的串聯(lián)、并聯(lián)組合方法，將基礎(chǔ)模塊合約整合為系統(tǒng)合約。由于SCADE搭建的系統(tǒng)用于處理連續(xù)的信號，同時系統(tǒng)內(nèi)部可能存在各種各樣的延時處理功能以及信號、狀態(tài)存儲功能，所以生成的系統(tǒng)合約可能需要處理后才能用于生成測試用例等工作。

6）生成測試用例

根據(jù)系統(tǒng)合約，分析系統(tǒng)可能存在的工作狀態(tài)，以此為基礎(chǔ)，為系統(tǒng)設(shè)計相應(yīng)的充分的測試用例；

7）生成測試腳本

根據(jù)SCADE軟件的測試腳本編寫方法，將生成的測試用例寫入測試腳本以便驗證測試用例；

8）生成期望輸出

通過將測試用例代人系統(tǒng)合約，為測試用例得出相應(yīng)的期望輸出。

4基于合約的SCADE測試工具運行實例

根據(jù)工具的初步設(shè)計與實現(xiàn)，我們?nèi)∫粋€簡單的復(fù)合模塊作為實例，對工具進(jìn)行簡單的驗證，并展示工具大概的測試流程。

我們?nèi)∽畲笾担∕AX）、自然對數(shù)（LNP）模塊進(jìn)行復(fù)合，用于求出兩個數(shù)中較大值的自然對數(shù)。我們假設(shè)模塊接口的狀態(tài)對模塊的值無影響，僅對模塊的數(shù)值計算部分做測試。

4.1MAX模塊接口與合約

模塊MAX用于出兩個輸出中的最大值。1）模塊接口如表1，包括輸入1、輸入2、輸出1等三個模塊接口；2）模塊值合約如表2，包含三條子合約，分別用于表示11.v>12.v、11.v=12.v和11.v<12.v等三種情況。

4.2 LNP模塊接口與合約

模塊LNP用于求輸入信號的自然對數(shù)。1）模塊接口如表3，包括輸入1、輸出1兩個模塊接口；2）模塊值合約如表4，包含一條子合約，用于對輸入信號進(jìn)行取對數(shù)操作。

4.3復(fù)合模塊接口與合約

由MAX模塊和LNP模塊符合成的符合模塊根據(jù)上述論文提到的方法進(jìn)行串聯(lián)組合，得到復(fù)合模塊的接口信息（表5）與組合合約（表6）。

1）模塊接口包括來自MAX模塊的輸入1、輸入2和來自LNP模塊的輸出1。2）模塊合約包括由MAX合約與LNP合約組合而成的兩條合約。

4.4復(fù)合模塊測試用例

根據(jù)復(fù)合模塊合約，我們得到三條用于對復(fù)合模塊進(jìn)行測試的測試用例（表7），每條測試用例對應(yīng)一條復(fù)合模塊合約。

4.5實例小結(jié)

此實例只列出簡單的模塊值的部分的合約組合方法，其他參數(shù)合約、狀態(tài)合約組合方法參照值合約的組合方法，然后將值、狀態(tài)與參數(shù)三項整合到一起，即得到整個系統(tǒng)的合約與測試用例。

5結(jié)束語

針對基于合約的SCADE模型的測試進(jìn)行了討論，目的是研究其測試過程自動化的可行性，闡述了工具的設(shè)計與實現(xiàn)等相關(guān)內(nèi)容。論文對基于合約的SCADE測試原理進(jìn)行了闡述，介紹了基于SCADE平臺所開發(fā)系統(tǒng)的合約生成策略。根據(jù)理論，設(shè)計了根據(jù)合約生成SCADE系統(tǒng)的測試用例的基本方法，并設(shè)計了測試工具對理論進(jìn)行實踐檢驗，同時列出了工具運行實例，基本證明了基于合約的SCADE測試工具的可行性。但是工具的設(shè)計并不完善，仍需進(jìn)行后續(xù)的研究與開發(fā)。