導(dǎo)航：安全管理網(wǎng)>> 安全論文>> 綜合安全論文>>正文

故障模型驅(qū)動(dòng)的軟件安全性測(cè)試研究

文檔作者：熊靜1 喻鋼2 4 徐中偉3 4 文檔來源： 1.上海工程技術(shù)大學(xué) 2.上海大學(xué) 3.同濟(jì)大學(xué) 4.鐵道部產(chǎn)品質(zhì)量監(jiān)督檢驗(yàn)中心		點(diǎn) 擊數(shù)：	更新時(shí)間： 2021年07月12日
下載地址：點(diǎn)擊這里	文件大?。?1.25 MB 共5頁	文檔格式： PDF	下載點(diǎn)數(shù)： 1 點(diǎn)（VIP免費(fèi)）

全屏查看

內(nèi)容預(yù)覽 [文件共5頁]

本文件共5頁，如需編輯使用，請(qǐng)下載。

注：預(yù)覽效果可能會(huì)出現(xiàn)部分文字亂碼（如口口口）、內(nèi)容顯示不全等問題，下載是正常的。

	文件大?。?.25 MB 共5頁文件格式：PDF 下載點(diǎn)數(shù)：1 點(diǎn)（VIP會(huì)員免費(fèi)）

下一篇：工業(yè)控制系統(tǒng)信息安全測(cè)試與防護(hù)技術(shù)趨勢(shì)

上一篇：基于安全控制邊界單元的IP核測(cè)試封裝方法

文本預(yù)覽

僅提取頁面文字內(nèi)容，供快速閱讀使用。

Computer Engineering and 2014，50（12） Applications計(jì)算機(jī)工程與應(yīng)用
1 引言
安全苛求軟件（Safety-Critical Software）一旦發(fā)生故
障或出現(xiàn)差錯(cuò)會(huì)使?jié)撛谖：υ囱葑兂刹豢山邮茱L(fēng)險(xiǎn)[1-2]。
高速鐵路列控中心軟件具有并發(fā)性、反應(yīng)式特性和行為
空間龐大的特點(diǎn)，研究適合描述軟件異常行為的建模方
法和故障相關(guān)測(cè)試用例生成方法，已經(jīng)成為列控中心軟
件的黑盒安全性測(cè)試?yán)碚摰难芯恐攸c(diǎn)。
2 相關(guān)研究
基于模型的測(cè)試是一種突破性的黑盒測(cè)試技術(shù)，它
以明確描述系統(tǒng)預(yù)期行為的抽象模型為依據(jù)，如故障模
型、安全模型、死鎖模型等，根據(jù)模型覆蓋測(cè)試準(zhǔn)則自動(dòng)
生成抽象的測(cè)試用例，自動(dòng)地產(chǎn)生測(cè)試腳本，執(zhí)行測(cè)試
并自動(dòng)評(píng)價(jià)測(cè)試結(jié)果，實(shí)現(xiàn)測(cè)試過程的完全自動(dòng)化[3-5]。
Offutt 和Liu[6]給出了從SOFL 形式規(guī)格說明產(chǎn)生測(cè)試用
例的步驟，并通過具體的實(shí)例詳細(xì)說明了測(cè)試用例產(chǎn)生
的過程。Offutt 等[7]還給出了一系列基于狀態(tài)規(guī)格說明
的測(cè)試準(zhǔn)則，用來指導(dǎo)基于狀態(tài)規(guī)格說明的系統(tǒng)測(cè)試。
OOWS[8]是一個(gè)模型驅(qū)動(dòng)的Web 應(yīng)用建模方法，強(qiáng)調(diào)
Web 應(yīng)用從需求獲取到模型建立，經(jīng)過模型轉(zhuǎn)換到最終
故障模型驅(qū)動(dòng)的軟件安全性測(cè)試研究
熊靜1，喻鋼2，4，徐中偉3，4
XIONG Jing1, YU Gang2，4, XU Zhongwei3，4
1.上海工程技術(shù)大學(xué)航空運(yùn)輸學(xué)院，上海201620
2.上海大學(xué)悉尼工商學(xué)院，上海201800
3.同濟(jì)大學(xué)電子與信息工程學(xué)院，上海201804
4.鐵道部產(chǎn)品質(zhì)量監(jiān)督檢驗(yàn)中心鐵路車站計(jì)算機(jī)聯(lián)鎖檢驗(yàn)站，上海201804
1.College of Air Transportation , Shanghai University of Engineering Science, Shanghai 201620, China
2.Sydney Institute of Language and Commerce, Shanghai University, Shanghai 201800, China
3.School of Electronics and Information Engineering, Tongji University, Shanghai 201804, China
4.Railway Station Computer Interlocking Test Station, Product Quality Supervision and Testing Center, Ministry of Railways,
Shanghai 201804, China
XIONG Jing, YU Gang, XU Zhongwei. Research on software safety test driven by fault model. Computer Engineering
and Applications, 2014, 50（12）：232-236.
Abstract：According to the requirements safety test, this paper establishes fault model to detect the safety logic fault, proposes
dynamic fault model generation algorithm and safety testing test generation algorithm based on fault coverage, which
can effectively identify the protection ability of software for fault safety. Its effectiveness is exemplified in safety testing
and validation of high-speed train control center in China.
Key words：high-speed railway; train control center; safety; formal modeling; safety test
摘要：根據(jù)安全性測(cè)試的需求，建立了檢測(cè)軟件內(nèi)部安全邏輯故障的故障模型，提出了故障模型動(dòng)態(tài)生成算法及
基于故障覆蓋的安全性測(cè)試生成算法，可以有效識(shí)別軟件是否具備對(duì)于故障的安全防護(hù)能力，在我國(guó)高速鐵路列控
中心安全性測(cè)試中說明了方法的有效性。
關(guān)鍵詞：高速鐵路；列控中心；安全性；形式化建模；安全性測(cè)試
文獻(xiàn)標(biāo)志碼：A 中圖分類號(hào)：TP391 doi：10.3778/j.issn.1002-8331.1305-0192
基金項(xiàng)目：國(guó)家自然科學(xué)基金（No.61075002）；國(guó)家“十二五”科技支撐計(jì)劃項(xiàng)目（No.2011BAG01B03）。
作者簡(jiǎn)介：熊靜（1979—），女，副教授，研究領(lǐng)域?yàn)榘踩燎筌浖问交Ｅc測(cè)試；喻鋼（1977—），男，博士，研究領(lǐng)域?yàn)榘踩?
求軟件形式化建模與測(cè)試；徐中偉（1964—），男，博士，教授，研究領(lǐng)域?yàn)榘踩燎筌浖问交?、仿真與測(cè)試。
E-mail：yugang509@163.com
收稿日期：2013-05-15 修回日期：2013-09-11 文章編號(hào)：1002-8331（2014）12-0232-05
CNKI 網(wǎng)絡(luò)優(yōu)先出版：2013-10-29，http://www.cnki.net/kcms/detail/11.2127.TP.20131029.1128.006.html
232
2014，50（12）
實(shí)現(xiàn)的開發(fā)全過程。文獻(xiàn)[9]提出使用符號(hào)執(zhí)行從類源
代碼抽取對(duì)象的狀態(tài)和行為，以一個(gè)四元組抽象描述
類，并轉(zhuǎn)化成等價(jià)的Kripke 結(jié)構(gòu)。使用CTL 公式描述測(cè)
試覆蓋標(biāo)準(zhǔn)進(jìn)行測(cè)試用例動(dòng)態(tài)生成。文獻(xiàn)[10]首先從
源程序建立UML 模型，通過UML 模型到LTS 模型的轉(zhuǎn)
換規(guī)則把UML 狀態(tài)圖轉(zhuǎn)換成這LTS 模型，然后通過路
徑轉(zhuǎn)換的生成流程生成路徑轉(zhuǎn)換序列，最后通過路徑轉(zhuǎn)
換生成測(cè)試用例并對(duì)程序進(jìn)行測(cè)試。
基于模型的軟件測(cè)試技術(shù)雖然近年來得到廣泛的
研究，但是在安全苛求領(lǐng)域中有一些問題依然沒有得到
很好的解決，最為集中的是誤報(bào)和漏報(bào)問題，主要由模型
定義和測(cè)試用例算法引起[11-12]。目前對(duì)于安全苛求軟件
的需求，尤其是安全性需求沒有一個(gè)規(guī)范的、統(tǒng)一的和形
式化的定義，其中故障模型的定義也不完備，導(dǎo)致后續(xù)產(chǎn)
生的測(cè)試用例集檢測(cè)得到的故障結(jié)果存在局限性。
3 安全行為模型定義
安全行為模型根據(jù)安全性需求的內(nèi)涵，利用安全因
子描述系統(tǒng)行為、系統(tǒng)狀態(tài)與系統(tǒng)危害之間的關(guān)系，采
用安全約束規(guī)則描述軟件行為的安全性約束，可以實(shí)現(xiàn)
對(duì)安全性需求更本質(zhì)的形式化定義。
定義1（安全行為模型） 安全行為模型是一個(gè)六元
組結(jié)構(gòu)S =< QA Λq0 Ω Π > ，其中：
（1）Q 是一個(gè)非空且有限的系統(tǒng)狀態(tài)集合，q0 為系
統(tǒng)的初始狀態(tài)。
（2）A 是一個(gè)可數(shù)的、可觀測(cè)的動(dòng)作標(biāo)記集合。包含：
① AI 表示有限非空的輸入動(dòng)作標(biāo)記集合，用“？”
表示；
② AO 表示有限非空的輸出動(dòng)作標(biāo)記集合，用“!”
表示；
③ Aτ 表示有限非空的內(nèi)部動(dòng)作標(biāo)記集合，用“#”
表示。
（3）Ω 是一個(gè)非空且有限的安全約束規(guī)則集合，用
于表示系統(tǒng)變遷的不同安全約束條件。
（4）Π 是一個(gè)非空且有限的安全因子集合。
（5）Λ 是一個(gè)非空且有限的系統(tǒng)變遷關(guān)系集合。其
中對(duì)于"t Î Λ 是一個(gè)具有如下結(jié)構(gòu)的六元組< qsa
bqd ρ α > ：
① qs 表示當(dāng)前變遷的起始狀態(tài)；
② a Î AI  Aτ 表示當(dāng)前變遷的輸入動(dòng)作標(biāo)記；
③ b Î AO  Aτ 表示當(dāng)前變遷的輸出動(dòng)作標(biāo)記；
④ qd 表示當(dāng)前變遷的目標(biāo)狀態(tài)；
⑤ ρ Î Ω 表示當(dāng)前變遷的安全約束規(guī)則；
⑥ α 為一個(gè)三元組< α
qs
s  α
qd
s  αt
s > Î Π ，其中α
qs
s 為
當(dāng)前變遷起始狀態(tài)的狀態(tài)安全因子，α
qd
s 為當(dāng)前變遷目
標(biāo)狀態(tài)的狀態(tài)安全因子，αt
s 為當(dāng)前變遷的變遷安全因子，
根據(jù)變遷安全因子的定義，后者可以通過狀態(tài)安全因子
計(jì)算獲得，因此也可以簡(jiǎn)記為一個(gè)二元組< α
qs
s  α
qd
s > 。
上述定義中，關(guān)于安全因子及安全約束規(guī)則的詳細(xì)
介紹參見文獻(xiàn)[13]。
定義2（擴(kuò)展安全行為模型） 給定安全行為模型S =
< QA Λq0 Ω Π >，則其擴(kuò)展模型記為Ext(S)，Ext(S) =
< Q′A′ Λ′q′0 Ω′ Π ′ > 為一個(gè)確定安全行為模型：
（1）Q′ = Q {unsafe safe} ，unsafe 為一個(gè)特殊的非
安全狀態(tài)，一旦系統(tǒng)進(jìn)入此狀態(tài)，表示系統(tǒng)發(fā)生了影響
安全性的失效行為，可能導(dǎo)致危害發(fā)生；safe 為一個(gè)特
殊的安全狀態(tài)，一旦系統(tǒng)進(jìn)入此狀態(tài)，表示系統(tǒng)行為符
合安全性需求。
（2）A′ = AI  AO {ω θ} ，ω θ 為一個(gè)外部可觀測(cè)
的特殊動(dòng)作標(biāo)記，ω θ Ï AI 且ω θ Ï AO 。
（3）Λ′ = ΛE lim(s) {q¾ ® ¾ ¾ ¾ ¾ ¾¾?ω ! ω:Æ: < αq
s αq
s >
safe|"a Î AI ,
b Î AO, ρ Î Ω Ø$q′ Î Q滿足
q¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾?a!b:ρ: < αq
s αq′
s >
q'} 
{q¾¾¾¾¾¾¾¾¾¾¾¾¾® ?a!b:Øρ: < αq
smax(αQ
s ) >
unsafe|$q′ Î Q,
a Î AIb Î Ao ρ Î Ω且
q¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾?a!b:ρ: < αq
s αq'
s >
q′} 
{q¾¾¾¾¾¾¾¾¾¾¾¾¾® ?θ ! θ:Øρ: < αq
smax(αQ
s ) >
unsafe|$q′,a Î AI ,b Î Ao,
ρ Î Ω且q¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾?a!b:ρ: < αq
s αq'
s >
q′a ¹ θb ¹ θ} 
{q¾¾¾¾¾¾¾¾¾¾¾¾¾® ?θ ! θ:Øρ: < αq
smax(αQ
s ) >
unsafe|$q′a Î AI
ρ Î Ω{q¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾?a!b:ρ: < αq
s αq′
s >
q′a ¹ θb ¹ θ} 
{q¾¾¾¾¾¾¾¾¾¾¾¾¾® ?θ ! θ:Øρ: < αq
s ,max(αQ
s ) >
unsafe|$q′,a Î AI ,b Î Ao,
ρ Î Ω且q¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾?a!b:ρ: < αq
s αq'
s >
q′a ¹ θb ¹ θ}
其中max(αQ
s ) 表示所有狀態(tài)安全因子中對(duì)應(yīng)風(fēng)險(xiǎn)等級(jí)
最高的因子。
（4）q′0 = q0 。
（5）Ω′ = Ω {Øρ|"ρ Î Ω} 。
（6）Π ′ = Π 。
擴(kuò)展安全行為模型不僅描述滿足安全性需求的正常
跡，同時(shí)通過引入safe 與unsafe 狀態(tài)、ω θ 動(dòng)作標(biāo)記及擴(kuò)
展安全約束規(guī)則，定義了不符合安全性需求的非安全跡。
4 安全苛求軟件故障模型
軟件安全性測(cè)試的目的是檢測(cè)出被測(cè)系統(tǒng)中存在
的可能導(dǎo)致風(fēng)險(xiǎn)，影響系統(tǒng)安全性的故障，因此對(duì)安全
性測(cè)試用例集的故障覆蓋度進(jìn)行分析和評(píng)價(jià)是十分必
要的[14]。影響系統(tǒng)安全性的故障一般源自軟件系統(tǒng)的
構(gòu)件內(nèi)部行為或構(gòu)件之間的交互行為中，這些行為的發(fā)
生之所以會(huì)影響系統(tǒng)安全性可以理解為其產(chǎn)生了不符合
安全性需求定義的輸出或者導(dǎo)致系統(tǒng)進(jìn)入了不符合安全
性需求定義的狀態(tài)。因此本文主要考慮如下故障模型：
熊靜，喻鋼，徐中偉：故障模型驅(qū)動(dòng)的軟件安全性測(cè)試研究233
Computer Engineering and 2014，50（12） Applications計(jì)算機(jī)工程與應(yīng)用
（1）輸出故障：在安全約束規(guī)則滿足或不滿足的前
提下，被測(cè)系統(tǒng)的安全行為模型中一個(gè)變遷的輸出發(fā)生
錯(cuò)誤，產(chǎn)生了不符合安全性需求的輸出。該故障可形式
化定義如下。
定義3（輸出故障） 假定安全性需求的安全行為模
型為I =< QA Λq0 Ω Π > ，被測(cè)系統(tǒng)的安全行為模型
為S =< QA Λq0 Ω Π > ，則FalutOutPut(IS) ={b|b Î
Ao $t1 Î Λs t2 Î ΛI(xiàn) t1 = < q1xyq'1 ρ1 < α
q1
s  α
q′1
s >>  t2 =
< q2abq′2 ρ2 < α
q2
s  α
q′2
s >>  q1 = q2 q′1 = q′2 x = a ρ1 =
ρ2 α
q1
s = α
q2
s  α
q′1
s = α
q′2
s y ¹ b} 。
（2）變遷故障：在安全約束規(guī)則滿足或不滿足的前
提下，被測(cè)系統(tǒng)的安全行為模型的一個(gè)變遷的末狀態(tài)發(fā)
生錯(cuò)誤，假設(shè)該故障不會(huì)增加安全行為模型的狀態(tài)數(shù)，
即故障的末狀態(tài)只是其他已有狀態(tài)，而不會(huì)是一個(gè)新引
入的狀態(tài)。該故障可形式化定義如下。
定義4（變遷故障） 假定安全性需求的安全行為模
型為I =< QA Λq0 Ω Π > ，被測(cè)系統(tǒng)的安全行為模型
為S =< Q,A, Λ,q0, Ω, Π >，則FalutTransit(IS) ={t|t Î ΛI(xiàn)
$t1 Î Λs t1 = < q1xyq′1 ρ1 < α
q1
s  α
q′1
s >>  t2 =< qabq′
ρ < αq
s αq′
s >> q1 = qx = ay = b ρ1 = ρ α
q1
s = αq
s α
q′1
s = αq′
s 
q′1 ¹ q′} 。
在安全性測(cè)試用例的生成中，理想的情況是希望生
成的安全性測(cè)試用例集能夠檢測(cè)出被測(cè)系統(tǒng)中存在的
所有故障，即包括單一故障、組合故障等情況，最終檢測(cè)
得到所有可能與安全性需求不一致的所有被測(cè)系統(tǒng)實(shí)
現(xiàn)。對(duì)于給定的安全性需求及其安全性測(cè)試用例集，本
文采用TS_FC(TSS) 表示測(cè)試用例集的故障覆蓋度，其
可通過如下方式計(jì)算獲得：
TS_FC(TSS) = FT(S) - FT(STS)
FT(S)
其中FT(S) 表示所有可能的故障模型數(shù)量，而FT(STS)
表示當(dāng)前安全性測(cè)試用例集能夠檢測(cè)出的故障數(shù)量。
5 基于故障模型的安全測(cè)試用例生成
當(dāng)系統(tǒng)中包含組合故障時(shí)，在故障數(shù)量越多的情況
下，越容易通過測(cè)試用例檢測(cè)出來，但是單一故障的存在
因?yàn)槠浒l(fā)生的概率較小不容易被檢測(cè)出來[15]，因此在本文
中僅考慮安全性測(cè)試用例集對(duì)于單一故障模型的覆蓋
度，即只考慮在被測(cè)安全苛求軟件的構(gòu)件級(jí)或系統(tǒng)級(jí)安
全行為模型只存在單一故障情況。一旦獲得系統(tǒng)單一故
障模型集合后，可以通過在每個(gè)故障模型上執(zhí)行安全性
測(cè)試用例集來驗(yàn)證其是否覆蓋故障模型。由于安全苛求
軟件的系統(tǒng)狀態(tài)及變遷數(shù)量可能非常龐大，安全性測(cè)試
用例集可能無法達(dá)到100%的故障覆蓋。因?yàn)橐环矫姘踩?
性測(cè)試用例集可能無法覆蓋某些系統(tǒng)變遷，因此安全性
測(cè)試用例集可能將無法檢測(cè)出由修改這些變遷得到的故
障，而另一方面對(duì)于安全性測(cè)試用例集覆蓋的系統(tǒng)變遷，
雖然能檢測(cè)到其是否產(chǎn)生了錯(cuò)誤的輸出，即能檢測(cè)到輸
出故障的發(fā)生，但是由于缺少對(duì)于安全性測(cè)試用例終止
狀態(tài)的驗(yàn)證，可能對(duì)由修改這些變遷得到的變遷錯(cuò)誤無
法被檢出。因此本文提出如下基于故障覆蓋的安全性測(cè)
試用例生成方法，以提高安全性測(cè)試用例的故障覆蓋度。
算法名稱：?jiǎn)我还收夏Ｐ蜕蒅en_FM
輸入：安全行為模型S
輸出：故障模型集合FM(S)
處理：
假定系統(tǒng)安全性需求S =< s1 s2 sn > ，其中si 表示構(gòu)
件i 的安全性需求對(duì)應(yīng)的安全行為模型，對(duì)于si = < QiAi Λi
q0 Ωi Πi > ，進(jìn)行如下處理：
for each 變遷t ，t Î Λi
對(duì)于當(dāng)前變遷t ，改變其末狀態(tài)，得到錯(cuò)誤變遷ft ，將其
代替變遷t ，即可獲得一個(gè)單一故障模型（變遷故障模型）FM -
Transit(si t ft)
將當(dāng)前故障模型FM - Transit(si t ft) 加入FM(S)
for each 變遷t ，t Î Λi
對(duì)于當(dāng)前變遷t ，改變輸出動(dòng)作標(biāo)記，得到錯(cuò)誤變遷ft ，
將其代替變遷t ，即可獲得一個(gè)單一故障模型（輸出故障模型）
FM - Output(si t ft)
將當(dāng)前故障模型FM - Output(si t ft) 加入FM(S)
算法名稱：GenSTC_FM算法
輸入：系統(tǒng)安全性需求的安全行為模型S ；安全性測(cè)試用
例集TS
輸出：擴(kuò)展安全性測(cè)試用例集EXT(TS)
處理：
Gen_FM(S) //生成故障模型集合；
For each FMi in FM(S)
{ Ext_TC(FMi) = Æ ；//將每個(gè)故障模型對(duì)應(yīng)的待擴(kuò)展安
全性測(cè)試用例集置為空
For each TCi in TS
{ Exec(FMiTCi) 將TCi 在FM 上執(zhí)行；
If（verdict (Exec(FMiTCi)) == safe）
{ If（ FMi 是變遷故障ÙTCi 包含F(xiàn)Mi 中的錯(cuò)誤變遷Ù
執(zhí)行后終止?fàn)顟B(tài)錯(cuò)誤）//表示當(dāng)前安全性測(cè)試用例TCi 未能檢
測(cè)到該故障
{ Ext_TC(FMi) = Ext_TC(FMi)  TCi ；}
}
Else
{ //表示當(dāng)前安全性測(cè)試用例TCi 能檢測(cè)到該故障
break；
}
}
}
For each FMi in FM(S)
{ If (Ext_TC(FMi) ¹ Æ Ù FMi 是變遷故障)
{ For each TCi in Ext_TC(FMi)
234
2014，50（12）
{ 獲得FMi 的終止?fàn)顟B(tài)驗(yàn)證跡Trace(Final_State) ；
TCi  Trace(Final_State) ® TCi'；//為當(dāng)前測(cè)試用例TCi
添加終止?fàn)顟B(tài)驗(yàn)證跡Trace(Final_State)，得到擴(kuò)展測(cè)試用例TCi'；
(TS -{TCi})  TCi ' ® TS ；//將擴(kuò)展后的安全性測(cè)試
用例替換其對(duì)應(yīng)的原測(cè)試用例
}
}
}
上述算法的時(shí)間復(fù)雜度與安全性測(cè)試用例集TS 和
安全性需求S 的規(guī)模成正比。其時(shí)間復(fù)雜度T(n) =
åi
= 1
n
|ΛTCi
| ×åj = 1
m
|Λj| × (|Qj| - 1) ，其中å
i = 1
n
|ΛTCi
| 表示安全性測(cè)試
用例集TS 的執(zhí)行時(shí)間，|ΛTCi
| 表示安全性測(cè)試用例TCi 的
變遷數(shù)量，å
j = 1
m
|Λj| × (|Qj| - 1) 表示被測(cè)系統(tǒng)的單一變遷故障
模型的數(shù)量，ΛjQj 表示變遷故障模型j 的變遷數(shù)量和
狀態(tài)數(shù)量。利用上述算法，對(duì)于每個(gè)變遷故障模型，依次
計(jì)算其與每個(gè)安全性測(cè)試用例的執(zhí)行結(jié)果，如果安全性
測(cè)試用例包含變遷故障所對(duì)應(yīng)的變遷并且又無法檢測(cè)出
該故障，則通過增加終止?fàn)顟B(tài)的驗(yàn)證跡將其進(jìn)行擴(kuò)展。
6 應(yīng)用實(shí)例
高速鐵路CTCS-2 列控中心能實(shí)現(xiàn)根據(jù)列車進(jìn)路和
軌道區(qū)段狀態(tài)等信息，通過信號(hào)安全數(shù)據(jù)網(wǎng)實(shí)現(xiàn)站內(nèi)和
區(qū)間軌道電路的載頻、低頻信息編碼功能，并控制軌道
電路的發(fā)碼方向。高速鐵路CTCS-2 列控中心的低頻信
息編碼功能是典型的安全相關(guān)功能，直接關(guān)系到列車運(yùn)
行安全。其安全行為模型見圖1。根據(jù)GenSTC_FM，
對(duì)應(yīng)的安全性測(cè)試用例集中部分安全性測(cè)試用例如下：
q4
q0
q1
q3 q12
q2
q13
q14
q15
q q16 11 q10 q9
q8
q5
?RouteNo!Φ
ρ1 GetRouteNo:→[Check(RouteNo)=true]
< αS
q
0 αs
q
1 >
?RouteNo!Signal
ρ11 CheckRouteOK:
→[Check(InWPXStation=true]
< αS
q
1 αs
q
3 >
?RouteNo!RouteType
ρ2 CheckRouteOK:
→[Check(InStation)=true]
< αS
q
1 αs
q
2 >
?RouteType
!’L5-L4-L4-L4’
ρ4 GetRouteType:
→[Check(RouteType=’ZXFC’
Ù Signal.State=’Open’)=true]
< αS
q
2 αs
q
5 >
?RouteType
!UU-Hu-Hu-Hu’
ρ4 GetRouteType:
→[Check(RouteType=’CXJC’
Ù Signal.State=’Open’
Ù Exist(12-Switch)=true)]
< αS
q
2 αs
q
6 >
?RouteType
!HB-B-B’
ρ9 GetRouteType:
→[Check(RouteType=’YDFC’
Ù Signal.State=’Open’)=true]
< αS
q
2 αs
q
10 >
?RouteType
!HB-Hu-L5’
ρ15 GetRouteType:
→[Check(RouteType=’YDJC’
Ù Signal.State=’Open’)=true]
< αS
q
3 αs
q
15 >
?RouteType
!HB-B-B-Hu’
ρ10 GetRouteType:
→[Check(RouteType=’YDJC’
Ù Signal.State=’Open’)=true]
< αS
q
2 αs
q
11 >
?RouteType
!U-Hu-Hu-L5’
ρ12 GetRouteType:
→[Check(InSignal.State=’Close’
Ù OutSignal.State=’Close’)=true]
< αS
q
3 αs
q
12 >
?RouteType
!U-Hu-L5’
ρ13 GetRouteType:
→[Check(InSignal.State=Open
Ù OutSignal.State=’Close’)=true]
< αS
q
3 αs
q
13 >
?RouteType
!L5-L5-L5’
ρ14 GetRouteType:
→[Check(InSignal.State=’Open’
Ù OutSignal.State=’Open’)=true]
< αS
q
3 αs
q
14 >
?RouteType
!UU-L5-L5-L5’
ρ6 GetRouteType:
→[Check(RouteType=’CXFC’
Ù Signal.State=’Open’
Ù Exist(12-Switch)=true)]
< αS
q
2 αs
q
7 >
?RouteType
!UUS-Hu-Hu-Hu’
ρ7 GetRouteType:
→[Check(RouteType=’CXJC’
Ù Signal.State=’Open’
Ù Exist(18-Switch)=true)]
< αS
q
2 αs
q
8 >
q7
q6
?RouteType
!’U-Hu-Hu-Hu’
ρ3 GetRouteType:
→[Check(RouteType=’ZXJC’
Ù Signal.State=’Open’)=true]
< αS
q
2 αs
q
4 >
?RouteType
!UU-Hu-Hu’
ρ8 GetRouteType:
→[Check(RouteType=’CXFC’
Ù Signal.State=’Open’
Ù Exist(18-Switch)=true)]
< αS
q
2 αs
q
9 >
?RouteType
!Hu-HB-L5’
ρ16 GetRouteType:
→[Check(RouteType=’YDFC’
Ù Signal.State=’Open’)=true]
< αS
q
3 αs
q
16 >
圖1 SBM_FM的安全行為模型
熊靜，喻鋼，徐中偉：故障模型驅(qū)動(dòng)的軟件安全性測(cè)試研究235
Computer Engineering and 2014，50（12） Applications計(jì)算機(jī)工程與應(yīng)用
q0¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo! Φ:Øρ1 unsafe
q0¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo! Φ:GetRouteNo: ®[Check(RouteNo) = true]
q1¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾¾¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾? RouteNo!RouteType ®[Øρ11]
unsafe
q0¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo! Φ:GetRouteNo: ®[Check(RouteNo) = true]
q1¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo!RouteType ®[ρ2]
q2¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾¾¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾?RouteType! 'U - HU - HU - HU′ ®[ρ3]
q4¾¾?¾ω!¾ω¾:Æ®safe
q0¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo! Φ:GetRouteNo: ®[Check(RouteNo) = true]
q1¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo!RouteType ®[ρ2]
q2¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteType! 'L5 - L4 - L4 - L4′ ®[ρ3]
q5¾¾?¾ω!¾ω¾:Æ®safe
q0¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo! Φ:GetRouteNo: ®[Check(RouteNo) = true]
q1¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo!RouteType ®[ρ2]
q2¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteType! 'UU - HU - HU - HU′ ®[ρ5]
q6¾¾?¾ω!¾ω¾:Æ®safe
q0¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo! Φ:GetRouteNo: ®[Check(RouteNo) = true]
q1¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo!RouteType ®[ρ2]
q2¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾?RouteType! 'UU - HU - HU - HU′ ®[Øρ5]
q6¾¾?¾ω!¾ω¾:Æ®unsafe
q0¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo! Φ:GetRouteNo: ®[Check(RouteNo) = true]
q1¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo!RouteType ®[ρ2]
q2¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾¾?RouteType! 'UUS - HU - HU - HU′ ®[Øρ7]
q7¾¾?¾ω!¾ω¾:Æ®unsafe
q0¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo! Φ:GetRouteNo: ®[Check(RouteNo) = true]
q1¾¾¾¾¾¾¾¾¾¾¾¾¾¾¾® ?RouteNo!RouteType ®[ρ2]
q2¾ ® ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾ ¾?RouteType! 'UUS - HU - HU - HU′ ®[ρ7]
q7¾¾?¾ω!¾ω¾:Æ®safe
……}
7 結(jié)束語
本文根據(jù)安全性測(cè)試的需求，建立了檢測(cè)軟件內(nèi)
部安全邏輯故障的故障模型，提出了故障模型動(dòng)態(tài)生
成算法及基于故障覆蓋的安全性測(cè)試生成算法，可以
有效識(shí)別軟件是否具備對(duì)于故障的安全防護(hù)能力，在
我國(guó)高速鐵路列控中心安全性測(cè)試中說明了方法的有
效性。
參考文獻(xiàn)：
[1] 鐵道部科技司.CTCS-級(jí)列控系統(tǒng)需求規(guī)范（SRS）[M].北
京：中國(guó)鐵道出版社，2008.
[2] 張曙光.CTCS-3 級(jí)列控系統(tǒng)總體技術(shù)方案[M].北京：中國(guó)
鐵道出版社，2008.
[3] 顏炯，王戟，陳火旺.基于模型的軟件測(cè)試綜述[J].計(jì)算機(jī)科
學(xué)，2004，31（2）：184-187.
[4] ISO/IEC 9646 Information processing system-open system
interconnection-OSI conformance testing methodology and
framework-part 1：general concepts[S].1994.
[5] 吳建平.基于形式化方法的一致性測(cè)試研究[D].北京：清華
大學(xué)，1997.
[6] Offutt A J，Liu S.Generating test data from SOFL specifications，
technical ISSE-TR-97-02[R].USA：Fairfax VA
Department of Information and Software Systems Engineering，
Mason University，1997.
[7] Offut A J，Liu S.Generating test data from state-based
specifications[J].The Journal of Software Testing，Verification，
and Reliability，2003，13（1）：25-53.
[8] Albert M，Peleehano V，F(xiàn)Ons J，et al.Extracting knowledge
from association relationships to build navigation
models[J].The Journal of Software Engineering，2004，12
（6）：25-53.
[9] 梁陳良，聶長(zhǎng)海，徐寶文，等.一種基于模型檢驗(yàn)的類測(cè)試
用例生成方法[J].東南大學(xué)學(xué)報(bào)：自然科學(xué)版，2007，37（5）：
184-187.
[10] 陳志德.基于模型的面向?qū)ο鬁y(cè)試用例生成研究[D].合
肥：中國(guó)科學(xué)技術(shù)大學(xué)，2010.
[11] 楊仕平，桑楠，熊光澤.安全關(guān)鍵軟件的防危性測(cè)評(píng)技術(shù)
研究[J].計(jì)算機(jī)學(xué)報(bào)，2004，27（3）：442-450.
[12] 徐中偉.安全軟件測(cè)試?yán)碚撆c技術(shù)的研究及其在鐵路信
號(hào)安全軟件測(cè)評(píng)中的實(shí)現(xiàn)[D].上海：同濟(jì)大學(xué)，2000.
[13] 喻鋼，劉曉文，熊靜，等.高速鐵路列控中心軟件安全性需
求形式化建模[J].鐵道學(xué)報(bào)，2013，35（6）：15-21.
[14] 張波.基于測(cè)試覆蓋的安全關(guān)鍵軟件測(cè)試策略研究[D].長(zhǎng)
春：中國(guó)科學(xué)院長(zhǎng)春光學(xué)精密機(jī)械與物理研究所，2012.
[15] 虞詡.基于黑箱測(cè)試及風(fēng)險(xiǎn)分析的鐵路信號(hào)控制軟件安
全性評(píng)估理論的研究與實(shí)踐[D].上海：同濟(jì)大學(xué)，2000.
236

網(wǎng)友評(píng)論 more

綜合安全論文最新內(nèi)容

04-10