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

故障模型驅動的軟件安全性測試研究

文檔作者：熊靜1 喻鋼2 4 徐中偉3 4 文檔來源： 1.上海工程技術大學 2.上海大學 3.同濟大學 4.鐵道部產(chǎn)品質量監(jiān)督檢驗中心			點擊數(shù)：
下載地址：點擊這里	文件大?。?1.25 MB 共5頁	文檔格式： PDF	下載點數(shù)： 1 點（VIP免費）

全屏查看

內容預覽 [文件共5頁]

本文件共5頁，如需編輯使用，請下載。

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

	文件大?。?.25 MB 共5頁文件格式：PDF 下載點數(shù)：1 點（VIP會員免費）

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

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

文本預覽

僅提取頁面文字內容，供快速閱讀使用。

Computer Engineering and 2014，50（12） Applications計算機工程與應用
1 引言
安全苛求軟件（Safety-Critical Software）一旦發(fā)生故
障或出現(xiàn)差錯會使?jié)撛谖：υ囱葑兂刹豢山邮茱L險[1-2]。
高速鐵路列控中心軟件具有并發(fā)性、反應式特性和行為
空間龐大的特點，研究適合描述軟件異常行為的建模方
法和故障相關測試用例生成方法，已經(jīng)成為列控中心軟
件的黑盒安全性測試理論的研究重點。
2 相關研究
基于模型的測試是一種突破性的黑盒測試技術，它
以明確描述系統(tǒng)預期行為的抽象模型為依據(jù)，如故障模
型、安全模型、死鎖模型等，根據(jù)模型覆蓋測試準則自動
生成抽象的測試用例，自動地產(chǎn)生測試腳本，執(zhí)行測試
并自動評價測試結果，實現(xiàn)測試過程的完全自動化[3-5]。
Offutt 和Liu[6]給出了從SOFL 形式規(guī)格說明產(chǎn)生測試用
例的步驟，并通過具體的實例詳細說明了測試用例產(chǎn)生
的過程。Offutt 等[7]還給出了一系列基于狀態(tài)規(guī)格說明
的測試準則，用來指導基于狀態(tài)規(guī)格說明的系統(tǒng)測試。
OOWS[8]是一個模型驅動的Web 應用建模方法，強調
Web 應用從需求獲取到模型建立，經(jīng)過模型轉換到最終
故障模型驅動的軟件安全性測試研究
熊靜1，喻鋼2，4，徐中偉3，4
XIONG Jing1, YU Gang2，4, XU Zhongwei3，4
1.上海工程技術大學航空運輸學院，上海201620
2.上海大學悉尼工商學院，上海201800
3.同濟大學電子與信息工程學院，上海201804
4.鐵道部產(chǎn)品質量監(jiān)督檢驗中心鐵路車站計算機聯(liá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ù)安全性測試的需求，建立了檢測軟件內部安全邏輯故障的故障模型，提出了故障模型動態(tài)生成算法及
基于故障覆蓋的安全性測試生成算法，可以有效識別軟件是否具備對于故障的安全防護能力，在我國高速鐵路列控
中心安全性測試中說明了方法的有效性。
關鍵詞：高速鐵路；列控中心；安全性；形式化建模；安全性測試
文獻標志碼：A 中圖分類號：TP391 doi：10.3778/j.issn.1002-8331.1305-0192
基金項目：國家自然科學基金（No.61075002）；國家“十二五”科技支撐計劃項目（No.2011BAG01B03）。
作者簡介：熊靜（1979—），女，副教授，研究領域為安全苛求軟件形式化建模與測試；喻鋼（1977—），男，博士，研究領域為安全苛
求軟件形式化建模與測試；徐中偉（1964—），男，博士，教授，研究領域為安全苛求軟件形式化建模、仿真與測試。
E-mail：yugang509@163.com
收稿日期：2013-05-15 修回日期：2013-09-11 文章編號：1002-8331（2014）12-0232-05
CNKI 網(wǎng)絡優(yōu)先出版：2013-10-29，http://www.cnki.net/kcms/detail/11.2127.TP.20131029.1128.006.html
232
2014，50（12）
實現(xiàn)的開發(fā)全過程。文獻[9]提出使用符號執(zhí)行從類源
代碼抽取對象的狀態(tài)和行為，以一個四元組抽象描述
類，并轉化成等價的Kripke 結構。使用CTL 公式描述測
試覆蓋標準進行測試用例動態(tài)生成。文獻[10]首先從
源程序建立UML 模型，通過UML 模型到LTS 模型的轉
換規(guī)則把UML 狀態(tài)圖轉換成這LTS 模型，然后通過路
徑轉換的生成流程生成路徑轉換序列，最后通過路徑轉
換生成測試用例并對程序進行測試。
基于模型的軟件測試技術雖然近年來得到廣泛的
研究，但是在安全苛求領域中有一些問題依然沒有得到
很好的解決，最為集中的是誤報和漏報問題，主要由模型
定義和測試用例算法引起[11-12]。目前對于安全苛求軟件
的需求，尤其是安全性需求沒有一個規(guī)范的、統(tǒng)一的和形
式化的定義，其中故障模型的定義也不完備，導致后續(xù)產(chǎn)
生的測試用例集檢測得到的故障結果存在局限性。
3 安全行為模型定義
安全行為模型根據(jù)安全性需求的內涵，利用安全因
子描述系統(tǒng)行為、系統(tǒng)狀態(tài)與系統(tǒng)危害之間的關系，采
用安全約束規(guī)則描述軟件行為的安全性約束，可以實現(xiàn)
對安全性需求更本質的形式化定義。
定義1（安全行為模型） 安全行為模型是一個六元
組結構S =< QA Λq0 Ω Π > ，其中：
（1）Q 是一個非空且有限的系統(tǒng)狀態(tài)集合，q0 為系
統(tǒng)的初始狀態(tài)。
（2）A 是一個可數(shù)的、可觀測的動作標記集合。包含：
① AI 表示有限非空的輸入動作標記集合，用“？”
表示；
② AO 表示有限非空的輸出動作標記集合，用“!”
表示；
③ Aτ 表示有限非空的內部動作標記集合，用“#”
表示。
（3）Ω 是一個非空且有限的安全約束規(guī)則集合，用
于表示系統(tǒng)變遷的不同安全約束條件。
（4）Π 是一個非空且有限的安全因子集合。
（5）Λ 是一個非空且有限的系統(tǒng)變遷關系集合。其
中對于"t Î Λ 是一個具有如下結構的六元組< qsa
bqd ρ α > ：
① qs 表示當前變遷的起始狀態(tài)；
② a Î AI  Aτ 表示當前變遷的輸入動作標記；
③ b Î AO  Aτ 表示當前變遷的輸出動作標記；
④ qd 表示當前變遷的目標狀態(tài)；
⑤ ρ Î Ω 表示當前變遷的安全約束規(guī)則；
⑥ α 為一個三元組< α
qs
s  α
qd
s  αt
s > Î Π ，其中α
qs
s 為
當前變遷起始狀態(tài)的狀態(tài)安全因子，α
qd
s 為當前變遷目
標狀態(tài)的狀態(tài)安全因子，αt
s 為當前變遷的變遷安全因子，
根據(jù)變遷安全因子的定義，后者可以通過狀態(tài)安全因子
計算獲得，因此也可以簡記為一個二元組< α
qs
s  α
qd
s > 。
上述定義中，關于安全因子及安全約束規(guī)則的詳細
介紹參見文獻[13]。
定義2（擴展安全行為模型） 給定安全行為模型S =
< QA Λq0 Ω Π >，則其擴展模型記為Ext(S)，Ext(S) =
< Q′A′ Λ′q′0 Ω′ Π ′ > 為一個確定安全行為模型：
（1）Q′ = Q {unsafe safe} ，unsafe 為一個特殊的非
安全狀態(tài)，一旦系統(tǒng)進入此狀態(tài)，表示系統(tǒng)發(fā)生了影響
安全性的失效行為，可能導致危害發(fā)生；safe 為一個特
殊的安全狀態(tài)，一旦系統(tǒng)進入此狀態(tài)，表示系統(tǒng)行為符
合安全性需求。
（2）A′ = AI  AO {ω θ} ，ω θ 為一個外部可觀測
的特殊動作標記，ω θ Ï 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)安全因子中對應風險等級
最高的因子。
（4）q′0 = q0 。
（5）Ω′ = Ω {Øρ|"ρ Î Ω} 。
（6）Π ′ = Π 。
擴展安全行為模型不僅描述滿足安全性需求的正常
跡，同時通過引入safe 與unsafe 狀態(tài)、ω θ 動作標記及擴
展安全約束規(guī)則，定義了不符合安全性需求的非安全跡。
4 安全苛求軟件故障模型
軟件安全性測試的目的是檢測出被測系統(tǒng)中存在
的可能導致風險，影響系統(tǒng)安全性的故障，因此對安全
性測試用例集的故障覆蓋度進行分析和評價是十分必
要的[14]。影響系統(tǒng)安全性的故障一般源自軟件系統(tǒng)的
構件內部行為或構件之間的交互行為中，這些行為的發(fā)
生之所以會影響系統(tǒng)安全性可以理解為其產(chǎn)生了不符合
安全性需求定義的輸出或者導致系統(tǒng)進入了不符合安全
性需求定義的狀態(tài)。因此本文主要考慮如下故障模型：
熊靜，喻鋼，徐中偉：故障模型驅動的軟件安全性測試研究233
Computer Engineering and 2014，50（12） Applications計算機工程與應用
（1）輸出故障：在安全約束規(guī)則滿足或不滿足的前
提下，被測系統(tǒng)的安全行為模型中一個變遷的輸出發(fā)生
錯誤，產(chǎn)生了不符合安全性需求的輸出。該故障可形式
化定義如下。
定義3（輸出故障） 假定安全性需求的安全行為模
型為I =< QA Λq0 Ω Π > ，被測系統(tǒng)的安全行為模型
為S =< QA Λq0 Ω Π > ，則FalutOutPut(IS) ={b|b Î
Ao $t1 Î Λs t2 Î ΛI 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ī)則滿足或不滿足的前
提下，被測系統(tǒng)的安全行為模型的一個變遷的末狀態(tài)發(fā)
生錯誤，假設該故障不會增加安全行為模型的狀態(tài)數(shù)，
即故障的末狀態(tài)只是其他已有狀態(tài)，而不會是一個新引
入的狀態(tài)。該故障可形式化定義如下。
定義4（變遷故障） 假定安全性需求的安全行為模
型為I =< QA Λq0 Ω Π > ，被測系統(tǒng)的安全行為模型
為S =< Q,A, Λ,q0, Ω, Π >，則FalutTransit(IS) ={t|t Î ΛI
$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′} 。
在安全性測試用例的生成中，理想的情況是希望生
成的安全性測試用例集能夠檢測出被測系統(tǒng)中存在的
所有故障，即包括單一故障、組合故障等情況，最終檢測
得到所有可能與安全性需求不一致的所有被測系統(tǒng)實
現(xiàn)。對于給定的安全性需求及其安全性測試用例集，本
文采用TS_FC(TSS) 表示測試用例集的故障覆蓋度，其
可通過如下方式計算獲得：
TS_FC(TSS) = FT(S) - FT(STS)
FT(S)
其中FT(S) 表示所有可能的故障模型數(shù)量，而FT(STS)
表示當前安全性測試用例集能夠檢測出的故障數(shù)量。
5 基于故障模型的安全測試用例生成
當系統(tǒng)中包含組合故障時，在故障數(shù)量越多的情況
下，越容易通過測試用例檢測出來，但是單一故障的存在
因為其發(fā)生的概率較小不容易被檢測出來[15]，因此在本文
中僅考慮安全性測試用例集對于單一故障模型的覆蓋
度，即只考慮在被測安全苛求軟件的構件級或系統(tǒng)級安
全行為模型只存在單一故障情況。一旦獲得系統(tǒng)單一故
障模型集合后，可以通過在每個故障模型上執(zhí)行安全性
測試用例集來驗證其是否覆蓋故障模型。由于安全苛求
軟件的系統(tǒng)狀態(tài)及變遷數(shù)量可能非常龐大，安全性測試
用例集可能無法達到100%的故障覆蓋。因為一方面安全
性測試用例集可能無法覆蓋某些系統(tǒng)變遷，因此安全性
測試用例集可能將無法檢測出由修改這些變遷得到的故
障，而另一方面對于安全性測試用例集覆蓋的系統(tǒng)變遷，
雖然能檢測到其是否產(chǎn)生了錯誤的輸出，即能檢測到輸
出故障的發(fā)生，但是由于缺少對于安全性測試用例終止
狀態(tài)的驗證，可能對由修改這些變遷得到的變遷錯誤無
法被檢出。因此本文提出如下基于故障覆蓋的安全性測
試用例生成方法，以提高安全性測試用例的故障覆蓋度。
算法名稱：單一故障模型生成Gen_FM
輸入：安全行為模型S
輸出：故障模型集合FM(S)
處理：
假定系統(tǒng)安全性需求S =< s1 s2 sn > ，其中si 表示構
件i 的安全性需求對應的安全行為模型，對于si = < QiAi Λi
q0 Ωi Πi > ，進行如下處理：
for each 變遷t ，t Î Λi
對于當前變遷t ，改變其末狀態(tài)，得到錯誤變遷ft ，將其
代替變遷t ，即可獲得一個單一故障模型（變遷故障模型）FM -
Transit(si t ft)
將當前故障模型FM - Transit(si t ft) 加入FM(S)
for each 變遷t ，t Î Λi
對于當前變遷t ，改變輸出動作標記，得到錯誤變遷ft ，
將其代替變遷t ，即可獲得一個單一故障模型（輸出故障模型）
FM - Output(si t ft)
將當前故障模型FM - Output(si t ft) 加入FM(S)
算法名稱：GenSTC_FM算法
輸入：系統(tǒng)安全性需求的安全行為模型S ；安全性測試用
例集TS
輸出：擴展安全性測試用例集EXT(TS)
處理：
Gen_FM(S) //生成故障模型集合；
For each FMi in FM(S)
{ Ext_TC(FMi) = Æ ；//將每個故障模型對應的待擴展安
全性測試用例集置為空
For each TCi in TS
{ Exec(FMiTCi) 將TCi 在FM 上執(zhí)行；
If（verdict (Exec(FMiTCi)) == safe）
{ If（ FMi 是變遷故障ÙTCi 包含F(xiàn)Mi 中的錯誤變遷Ù
執(zhí)行后終止狀態(tài)錯誤）//表示當前安全性測試用例TCi 未能檢
測到該故障
{ Ext_TC(FMi) = Ext_TC(FMi)  TCi ；}
}
Else
{ //表示當前安全性測試用例TCi 能檢測到該故障
break；
}
}
}
For each FMi in FM(S)
{ If (Ext_TC(FMi) ¹ Æ Ù FMi 是變遷故障)
{ For each TCi in Ext_TC(FMi)
234
2014，50（12）
{ 獲得FMi 的終止狀態(tài)驗證跡Trace(Final_State) ；
TCi  Trace(Final_State) ® TCi'；//為當前測試用例TCi
添加終止狀態(tài)驗證跡Trace(Final_State)，得到擴展測試用例TCi'；
(TS -{TCi})  TCi ' ® TS ；//將擴展后的安全性測試
用例替換其對應的原測試用例
}
}
}
上述算法的時間復雜度與安全性測試用例集TS 和
安全性需求S 的規(guī)模成正比。其時間復雜度T(n) =
åi
= 1
n
|ΛTCi
| ×åj = 1
m
|Λj| × (|Qj| - 1) ，其中å
i = 1
n
|ΛTCi
| 表示安全性測試
用例集TS 的執(zhí)行時間，|ΛTCi
| 表示安全性測試用例TCi 的
變遷數(shù)量，å
j = 1
m
|Λj| × (|Qj| - 1) 表示被測系統(tǒng)的單一變遷故障
模型的數(shù)量，ΛjQj 表示變遷故障模型j 的變遷數(shù)量和
狀態(tài)數(shù)量。利用上述算法，對于每個變遷故障模型，依次
計算其與每個安全性測試用例的執(zhí)行結果，如果安全性
測試用例包含變遷故障所對應的變遷并且又無法檢測出
該故障，則通過增加終止狀態(tài)的驗證跡將其進行擴展。
6 應用實例
高速鐵路CTCS-2 列控中心能實現(xiàn)根據(jù)列車進路和
軌道區(qū)段狀態(tài)等信息，通過信號安全數(shù)據(jù)網(wǎng)實現(xiàn)站內和
區(qū)間軌道電路的載頻、低頻信息編碼功能，并控制軌道
電路的發(fā)碼方向。高速鐵路CTCS-2 列控中心的低頻信
息編碼功能是典型的安全相關功能，直接關系到列車運
行安全。其安全行為模型見圖1。根據(jù)GenSTC_FM，
對應的安全性測試用例集中部分安全性測試用例如下：
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的安全行為模型
熊靜，喻鋼，徐中偉：故障模型驅動的軟件安全性測試研究235
Computer Engineering and 2014，50（12） Applications計算機工程與應用
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 結束語
本文根據(jù)安全性測試的需求，建立了檢測軟件內
部安全邏輯故障的故障模型，提出了故障模型動態(tài)生
成算法及基于故障覆蓋的安全性測試生成算法，可以
有效識別軟件是否具備對于故障的安全防護能力，在
我國高速鐵路列控中心安全性測試中說明了方法的有
效性。
參考文獻：
[1] 鐵道部科技司.CTCS-級列控系統(tǒng)需求規(guī)范（SRS）[M].北
京：中國鐵道出版社，2008.
[2] 張曙光.CTCS-3 級列控系統(tǒng)總體技術方案[M].北京：中國
鐵道出版社，2008.
[3] 顏炯，王戟，陳火旺.基于模型的軟件測試綜述[J].計算機科
學，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] 吳建平.基于形式化方法的一致性測試研究[D].北京：清華
大學，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] 梁陳良，聶長海，徐寶文，等.一種基于模型檢驗的類測試
用例生成方法[J].東南大學學報：自然科學版，2007，37（5）：
184-187.
[10] 陳志德.基于模型的面向對象測試用例生成研究[D].合
肥：中國科學技術大學，2010.
[11] 楊仕平，桑楠，熊光澤.安全關鍵軟件的防危性測評技術
研究[J].計算機學報，2004，27（3）：442-450.
[12] 徐中偉.安全軟件測試理論與技術的研究及其在鐵路信
號安全軟件測評中的實現(xiàn)[D].上海：同濟大學，2000.
[13] 喻鋼，劉曉文，熊靜，等.高速鐵路列控中心軟件安全性需
求形式化建模[J].鐵道學報，2013，35（6）：15-21.
[14] 張波.基于測試覆蓋的安全關鍵軟件測試策略研究[D].長
春：中國科學院長春光學精密機械與物理研究所，2012.
[15] 虞詡.基于黑箱測試及風險分析的鐵路信號控制軟件安
全性評估理論的研究與實踐[D].上海：同濟大學，2000.
236

網(wǎng)友評論 more

綜合安全論文最新內容

02-06