导航：安全管理网>> 安全论文>> 综合安全论文>>正文

故障模型驱动的软件安全性测试研究

文档作者：熊静1 喻钢2 4 徐中伟3 4 文档来源： 1.上海工程技术大学 2.上海大学 3.同济大学 4.铁道部产品质量监督检验中心		点击数：	更新时间： 2021年07月12日
下载地址：点击这里	文件大小： 1.25 MB 共5页	文档格式： PDF	下载点数： 1 点（VIP免费）

全屏查看

内容预览 [文件共5页]

本文件共5页，如需编辑使用，请下载。

注：预览效果可能会出现部分文字乱码（如口口口）、内容显示不全等问题，下载是正常的。

	文件大小：1.25 MB 共5页文件格式：PDF 下载点数：1 点（VIP会员免费）

下一篇：工业控制系统信息安全测试与防护技术趋势

上一篇：基于安全控制边界单元的IP核测试封装方法

文本预览

仅提取页面文字内容，供快速阅读使用。

Computer Engineering and 2014，50（12） Applications计算机工程与应用
1 引言
安全苛求软件（Safety-Critical Software）一旦发生故
障或出现差错会使潜在危害源演变成不可接受风险[1-2]。
高速铁路列控中心软件具有并发性、反应式特性和行为
空间庞大的特点，研究适合描述软件异常行为的建模方
法和故障相关测试用例生成方法，已经成为列控中心软
件的黑盒安全性测试理论的研究重点。
2 相关研究
基于模型的测试是一种突破性的黑盒测试技术，它
以明确描述系统预期行为的抽象模型为依据，如故障模
型、安全模型、死锁模型等，根据模型覆盖测试准则自动
生成抽象的测试用例，自动地产生测试脚本，执行测试
并自动评价测试结果，实现测试过程的完全自动化[3-5]。
Offutt 和Liu[6]给出了从SOFL 形式规格说明产生测试用
例的步骤，并通过具体的实例详细说明了测试用例产生
的过程。Offutt 等[7]还给出了一系列基于状态规格说明
的测试准则，用来指导基于状态规格说明的系统测试。
OOWS[8]是一个模型驱动的Web 应用建模方法，强调
Web 应用从需求获取到模型建立，经过模型转换到最终
故障模型驱动的软件安全性测试研究
熊静1，喻钢2，4，徐中伟3，4
XIONG Jing1, YU Gang2，4, XU Zhongwei3，4
1.上海工程技术大学航空运输学院，上海201620
2.上海大学悉尼工商学院，上海201800
3.同济大学电子与信息工程学院，上海201804
4.铁道部产品质量监督检验中心铁路车站计算机联锁检验站，上海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
摘要：根据安全性测试的需求，建立了检测软件内部安全逻辑故障的故障模型，提出了故障模型动态生成算法及
基于故障覆盖的安全性测试生成算法，可以有效识别软件是否具备对于故障的安全防护能力，在我国高速铁路列控
中心安全性测试中说明了方法的有效性。
关键词：高速铁路；列控中心；安全性；形式化建模；安全性测试
文献标志码：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 网络优先出版：2013-10-29，http://www.cnki.net/kcms/detail/11.2127.TP.20131029.1128.006.html
232
2014，50（12）
实现的开发全过程。文献[9]提出使用符号执行从类源
代码抽取对象的状态和行为，以一个四元组抽象描述
类，并转化成等价的Kripke 结构。使用CTL 公式描述测
试覆盖标准进行测试用例动态生成。文献[10]首先从
源程序建立UML 模型，通过UML 模型到LTS 模型的转
换规则把UML 状态图转换成这LTS 模型，然后通过路
径转换的生成流程生成路径转换序列，最后通过路径转
换生成测试用例并对程序进行测试。
基于模型的软件测试技术虽然近年来得到广泛的
研究，但是在安全苛求领域中有一些问题依然没有得到
很好的解决，最为集中的是误报和漏报问题，主要由模型
定义和测试用例算法引起[11-12]。目前对于安全苛求软件
的需求，尤其是安全性需求没有一个规范的、统一的和形
式化的定义，其中故障模型的定义也不完备，导致后续产
生的测试用例集检测得到的故障结果存在局限性。
3 安全行为模型定义
安全行为模型根据安全性需求的内涵，利用安全因
子描述系统行为、系统状态与系统危害之间的关系，采
用安全约束规则描述软件行为的安全性约束，可以实现
对安全性需求更本质的形式化定义。
定义1（安全行为模型） 安全行为模型是一个六元
组结构S =< QA Λq0 Ω Π > ，其中：
（1）Q 是一个非空且有限的系统状态集合，q0 为系
统的初始状态。
（2）A 是一个可数的、可观测的动作标记集合。包含：
① AI 表示有限非空的输入动作标记集合，用“？”
表示；
② AO 表示有限非空的输出动作标记集合，用“!”
表示；
③ Aτ 表示有限非空的内部动作标记集合，用“#”
表示。
（3）Ω 是一个非空且有限的安全约束规则集合，用
于表示系统变迁的不同安全约束条件。
（4）Π 是一个非空且有限的安全因子集合。
（5）Λ 是一个非空且有限的系统变迁关系集合。其
中对于"t Î Λ 是一个具有如下结构的六元组< qsa
bqd ρ α > ：
① qs 表示当前变迁的起始状态；
② a Î AI  Aτ 表示当前变迁的输入动作标记；
③ b Î AO  Aτ 表示当前变迁的输出动作标记；
④ qd 表示当前变迁的目标状态；
⑤ ρ Î Ω 表示当前变迁的安全约束规则；
⑥ α 为一个三元组< α
qs
s  α
qd
s  αt
s > Î Π ，其中α
qs
s 为
当前变迁起始状态的状态安全因子，α
qd
s 为当前变迁目
标状态的状态安全因子，αt
s 为当前变迁的变迁安全因子，
根据变迁安全因子的定义，后者可以通过状态安全因子
计算获得，因此也可以简记为一个二元组< α
qs
s  α
qd
s > 。
上述定义中，关于安全因子及安全约束规则的详细
介绍参见文献[13]。
定义2（扩展安全行为模型） 给定安全行为模型S =
< QA Λq0 Ω Π >，则其扩展模型记为Ext(S)，Ext(S) =
< Q′A′ Λ′q′0 Ω′ Π ′ > 为一个确定安全行为模型：
（1）Q′ = Q {unsafe safe} ，unsafe 为一个特殊的非
安全状态，一旦系统进入此状态，表示系统发生了影响
安全性的失效行为，可能导致危害发生；safe 为一个特
殊的安全状态，一旦系统进入此状态，表示系统行为符
合安全性需求。
（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 ) 表示所有状态安全因子中对应风险等级
最高的因子。
（4）q′0 = q0 。
（5）Ω′ = Ω {Øρ|"ρ Î Ω} 。
（6）Π ′ = Π 。
扩展安全行为模型不仅描述满足安全性需求的正常
迹，同时通过引入safe 与unsafe 状态、ω θ 动作标记及扩
展安全约束规则，定义了不符合安全性需求的非安全迹。
4 安全苛求软件故障模型
软件安全性测试的目的是检测出被测系统中存在
的可能导致风险，影响系统安全性的故障，因此对安全
性测试用例集的故障覆盖度进行分析和评价是十分必
要的[14]。影响系统安全性的故障一般源自软件系统的
构件内部行为或构件之间的交互行为中，这些行为的发
生之所以会影响系统安全性可以理解为其产生了不符合
安全性需求定义的输出或者导致系统进入了不符合安全
性需求定义的状态。因此本文主要考虑如下故障模型：
熊静，喻钢，徐中伟：故障模型驱动的软件安全性测试研究233
Computer Engineering and 2014，50（12） Applications计算机工程与应用
（1）输出故障：在安全约束规则满足或不满足的前
提下，被测系统的安全行为模型中一个变迁的输出发生
错误，产生了不符合安全性需求的输出。该故障可形式
化定义如下。
定义3（输出故障） 假定安全性需求的安全行为模
型为I =< QA Λq0 Ω Π > ，被测系统的安全行为模型
为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）变迁故障：在安全约束规则满足或不满足的前
提下，被测系统的安全行为模型的一个变迁的末状态发
生错误，假设该故障不会增加安全行为模型的状态数，
即故障的末状态只是其他已有状态，而不会是一个新引
入的状态。该故障可形式化定义如下。
定义4（变迁故障） 假定安全性需求的安全行为模
型为I =< QA Λq0 Ω Π > ，被测系统的安全行为模型
为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′} 。
在安全性测试用例的生成中，理想的情况是希望生
成的安全性测试用例集能够检测出被测系统中存在的
所有故障，即包括单一故障、组合故障等情况，最终检测
得到所有可能与安全性需求不一致的所有被测系统实
现。对于给定的安全性需求及其安全性测试用例集，本
文采用TS_FC(TSS) 表示测试用例集的故障覆盖度，其
可通过如下方式计算获得：
TS_FC(TSS) = FT(S) - FT(STS)
FT(S)
其中FT(S) 表示所有可能的故障模型数量，而FT(STS)
表示当前安全性测试用例集能够检测出的故障数量。
5 基于故障模型的安全测试用例生成
当系统中包含组合故障时，在故障数量越多的情况
下，越容易通过测试用例检测出来，但是单一故障的存在
因为其发生的概率较小不容易被检测出来[15]，因此在本文
中仅考虑安全性测试用例集对于单一故障模型的覆盖
度，即只考虑在被测安全苛求软件的构件级或系统级安
全行为模型只存在单一故障情况。一旦获得系统单一故
障模型集合后，可以通过在每个故障模型上执行安全性
测试用例集来验证其是否覆盖故障模型。由于安全苛求
软件的系统状态及变迁数量可能非常庞大，安全性测试
用例集可能无法达到100%的故障覆盖。因为一方面安全
性测试用例集可能无法覆盖某些系统变迁，因此安全性
测试用例集可能将无法检测出由修改这些变迁得到的故
障，而另一方面对于安全性测试用例集覆盖的系统变迁，
虽然能检测到其是否产生了错误的输出，即能检测到输
出故障的发生，但是由于缺少对于安全性测试用例终止
状态的验证，可能对由修改这些变迁得到的变迁错误无
法被检出。因此本文提出如下基于故障覆盖的安全性测
试用例生成方法，以提高安全性测试用例的故障覆盖度。
算法名称：单一故障模型生成Gen_FM
输入：安全行为模型S
输出：故障模型集合FM(S)
处理：
假定系统安全性需求S =< s1 s2 sn > ，其中si 表示构
件i 的安全性需求对应的安全行为模型，对于si = < QiAi Λi
q0 Ωi Πi > ，进行如下处理：
for each 变迁t ，t Î Λi
对于当前变迁t ，改变其末状态，得到错误变迁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算法
输入：系统安全性需求的安全行为模型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 上执行；
If（verdict (Exec(FMiTCi)) == safe）
{ If（ FMi 是变迁故障ÙTCi 包含FMi 中的错误变迁Ù
执行后终止状态错误）//表示当前安全性测试用例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 的终止状态验证迹Trace(Final_State) ；
TCi  Trace(Final_State) ® TCi'；//为当前测试用例TCi
添加终止状态验证迹Trace(Final_State)，得到扩展测试用例TCi'；
(TS -{TCi})  TCi ' ® TS ；//将扩展后的安全性测试
用例替换其对应的原测试用例
}
}
}
上述算法的时间复杂度与安全性测试用例集TS 和
安全性需求S 的规模成正比。其时间复杂度T(n) =
åi
= 1
n
|ΛTCi
| ×åj = 1
m
|Λj| × (|Qj| - 1) ，其中å
i = 1
n
|ΛTCi
| 表示安全性测试
用例集TS 的执行时间，|ΛTCi
| 表示安全性测试用例TCi 的
变迁数量，å
j = 1
m
|Λj| × (|Qj| - 1) 表示被测系统的单一变迁故障
模型的数量，ΛjQj 表示变迁故障模型j 的变迁数量和
状态数量。利用上述算法，对于每个变迁故障模型，依次
计算其与每个安全性测试用例的执行结果，如果安全性
测试用例包含变迁故障所对应的变迁并且又无法检测出
该故障，则通过增加终止状态的验证迹将其进行扩展。
6 应用实例
高速铁路CTCS-2 列控中心能实现根据列车进路和
轨道区段状态等信息，通过信号安全数据网实现站内和
区间轨道电路的载频、低频信息编码功能，并控制轨道
电路的发码方向。高速铁路CTCS-2 列控中心的低频信
息编码功能是典型的安全相关功能，直接关系到列车运
行安全。其安全行为模型见图1。根据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 结束语
本文根据安全性测试的需求，建立了检测软件内
部安全逻辑故障的故障模型，提出了故障模型动态生
成算法及基于故障覆盖的安全性测试生成算法，可以
有效识别软件是否具备对于故障的安全防护能力，在
我国高速铁路列控中心安全性测试中说明了方法的有
效性。
参考文献：
[1] 铁道部科技司.CTCS-级列控系统需求规范（SRS）[M].北
京：中国铁道出版社，2008.
[2] 张曙光.CTCS-3 级列控系统总体技术方案[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，FOns 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] 徐中伟.安全软件测试理论与技术的研究及其在铁路信
号安全软件测评中的实现[D].上海：同济大学，2000.
[13] 喻钢，刘晓文，熊静，等.高速铁路列控中心软件安全性需
求形式化建模[J].铁道学报，2013，35（6）：15-21.
[14] 张波.基于测试覆盖的安全关键软件测试策略研究[D].长
春：中国科学院长春光学精密机械与物理研究所，2012.
[15] 虞诩.基于黑箱测试及风险分析的铁路信号控制软件安
全性评估理论的研究与实践[D].上海：同济大学，2000.
236

网友评论 more

综合安全论文最新内容

05-04