2024年3月12日发(作者：)
计算机科学
2006Vol
1
33
№1
12
基于抽象2验证2细化范例的软件模型检测
3
)
刘吉锋 孙吉贵
(
吉林大学计算机科学与技术学院 长春
130012
)
(
吉林大学符号计算与知识工程教育部重点实验室 长春
130012
)
摘 要 如何保证软件系统的正确性和可靠性是当前软件开发面临的主要问题之一。模型检测作为一种重要的自动
化验证技术在软件的分析与验证中正取得越来越多的成功。本文以微软的
SLAM
和加州大学伯克利分校的
BLAST
为例综述性地介绍了基于抽象2验证2细化范例的软件模型检测。
关键词 模型检测
,
软件模型检测
,
谓词抽象
,
反例驱动的细化
SoftwareModelCheckingBasedonAbstract
2
verify
2
refineParadigm
LIUJi
2
Feng
SUNJi
2
Gui
(
CollegeofComputerScienceandTechnology,JilinUniversity,Changchun130012
)
(
KeyLaboratoryofSymbolicComputationandKnowledgeEngineerofMinistryofEducation,Changchun130012
)
Abstract
Howtoassurethecorrectnessandreliabilityofsoftwaresystemsisoneofthemainproblemsinsoftwarede
2
nimportantautomaticverificationtechnique,Modelcheckingismoreandmoresuccessfulinsoft
2
perpresentsasurveytosoftwaremodelcheckingbasedonabstract
2
verify
2
refine
paradigm,usingSLAMatMicrosoftandBLASTatUCBerkeleyasexamples.
Keywords
Modelchecking,Softwaremodelchecking,Predicateabstraction,Counterexample
2
drivenrefinement
1
引言
软件开发所面临的主要问题之一是如何保证系统的正确
性和可靠性
,
形式化方法是解决这个问题的重要途径。在诸
多形式化方法中
,
模型检测作为一种重要的自动化验证技术
已经在硬件和协议验证领域取得了巨大的成功
,
把模型检测
应用于软件验证已经成为近年来的一个焦点
,
并且已经取得
了一些成就
,
可以验证几十万行代码。
模型检测的思想是建立系统的模型
,
把系统中变量的取
值情况作为系统的状态
,
从指定初始状态开始根据状态转换
关系生成状态转换路径
,
代表系统的运行情况
;
把被验证属性
表示为状态转换路径必须满足的具体要求
,
如果状态转换路
径满足这种要求
,
则系统满足被验证属性
,
验证结束
,
否则
,
系
统不满足被验证属性
,
生成反例路径证明被验证属性如何被
破坏。
模型检测基于对系统状态空间进行穷举搜索
,
但直接对
无限状态系统或巨大的有限状态系统进行穷举搜索是不可行
的
,
另一方面
,
由于许多状态与被验证属性无关
,
这样做也是
不必要的
,
所以
,
模型检测工具通常工作在系统的抽象模型之
上。但抽象模型有时与系统不一致
,
所以
,
如果在验证过程中
发现抽象模型有问题
,
则需要对它做出相应调整。
软件属于无限状态系统
,
基于抽象2验证2细化范例的方
法
[1
～
3]
是一种通常的软件模型检测方法。
(
1
)
抽象
:
抽象的表示程序的具体状态
,
建立给定程序的
抽象模型
;
(
2
)
验证
:
对于被验证属性自动的验证抽象模型
,
如果比
给定程序粗糙的抽象模型没有破坏属性
,
那么给定程序也不
会破坏属性
,
于是返回“程序正确”
;
否则
,
自动产生一个抽象
反例路径
,
证明模型如何破坏属性
;
(
3
)
细化
:
自动检测抽象反例路径是否对应一个程序中的
具体反例
,
如果存在具体反例
,
则找到了一个程序错误
;
否则
,
表明抽象模型过于粗糙
,
不包含证明程序满足被验证属性所
需的足够信息
,
于是增加信息
,
使得步骤
(
1
)
可以抽象出更精
密的抽象模型
;goto
(
1
)
。
本文以微软的
SLAM
[1]
和加州大学伯克利分校的
BLAST
[4]
为例介绍基于抽象2验证2细化范例的软件模型检
测。
SLAM
和
BLAST
是用于验证
C
语言程序安全性属性的
模型检测工具
,
整个过程可以不依赖使用者提供辅助信息。
SLAM
把抽象2验证2细化三步循环分别用三个工具来实现
,
BLAST
则把这三步集成在一起。
本文的第
2
、
3
、
4
节分别介绍抽象、验证和细化
,
第
5
节介
绍
BLAST
如何把这三步循环集成在一起以及
BLAST
所使
用的基于克雷格插值的反例驱动的细化
,
第
6
节是相关工作
,
最后是结论。
2
抽象
软件模型检测使用的抽象技术是谓词抽象
[5,6]
,
思想是
把系统中数量众多的具体状态根据某方面的共性映射为数量
少得多的抽象状态
,
以便于模型检测器处理
;
这些共性用谓词
来表示
,
抽象状态用谓词的布尔组合来表示。谓词抽象已经
被应用于硬件和协议的验证
,
现在被用于验证软件
[4,7
～
9]
。
3
)
国家自然科学基金
(
60473003
)
、教育部“新世纪优秀人才支持计划”、博士点基金
(
2
)
资助课题。刘吉锋 硕士研究生
,
主要研究
方向是模型检测
;
孙吉贵 博士生导师
,
主要研究方向是人工智能、约束程序、决策支持系统。
・
255
・
SLAM
中用工具
C2BP
[8,10]
来进行谓词抽象。
C2BP
把
给定的
C
语言程序
P
根据谓词集合
E
抽象为布尔程序
[11]
BP
(
P,E
)
。
E
可以人为给定
,
但在细化阶段相应的工具会向
E
中增加谓词
,
所以
E
初始也可以为空。
E
中的谓词是
P
中变
量和常量构成的
C
语言布尔表达式。
P
中任何可行的执行路
径在
BP
(
P,E
)
中仍是可行的执行路径。
BP
(
P,E
)
拥有与
P
相同的控制结构
,
但只包含布尔变量
,
一个布尔变量代表一个
谓词。例如在图
1
中。对于
(
a
)
中的程序
P
和谓词集合
E=
{x==
’
x,x==
’
x+1,x<4,a==2,b==3},
可以生成
量
,
它的取值等于对应谓词的取值
,
表示
P
中语句的执行对
谓词
(
a==2
)
取值情况的影响
,
有
true
、
false
和3三种情况
,
3表示不确定。之所以会出现不确定
,
是因为根据当前谓词
集合有时不知道一条语句的执行对相关谓词有什么影响。例
如对一条语句“
curr=nextCurr;
”
,
其中
curr
和
nextCurr
是指
针变量
,
当前谓词集合中包含一个谓词
(
curr==NULL
)
,
但
不包含任何涉及
nextCurr
的谓词
,
则在这条语句执行后
,
由
于当前谓词集合不包含任何关于
nextCurr
的信息
,
所以谓词
(
curr==NULL
)
的真值无法判定
,
所以把对应布尔变量赋值
为3。对于取值为3的谓词
,
随机地认为它的真值为
true
或
false
。
图
1
(
b
)
中的布尔程序
BP
(
P,E
)
。
在
BP
(
P,E
)
中
,{a==2}
是代表谓词
(
a==2
)
的布尔变
图
1
BP
(
P,E
)
中“
{x==
’
x},{x==
’
x+1}=false,true;
”
表示对两个布尔变量的连续赋值。
有些语句不对任何谓词的取值产生影响
,
比如语句“
c=
0;
”
,
在
BP
(
P,E
)
中抽象为
skip
。
对于影响谓词取值的语句
,
如语句“
a=0;
”
,
在
BP
(
P,E
)
中抽象为对相关布尔变量赋值的语句。一个谓词在一条语句
执行后的取值取决于它的最弱前置条件。如果一个谓词
(
或
它的非
)
的最弱前置条件在语句执行前被蕴含
,
则这个谓词在
语句执行后真值为
true
(
或
false
)
。例如语句“
a=0;
”
,
在
BP
(
P,E
)
中对应语句“
{a==2}=true;
”。因为一个指针的间接
引用可能是一个变量的别名
,
所以计算最弱前置条件时要考
虑这种情况。例如计算
WP
(
x=5,
3
y>6
)
,
要考虑
y
是否是
指向
x
的指针
,
所以此时
WP
(
x=5,
3
y>6
)
=
((
&x=y
)
∧
(
5>6
))
∨
((
&x!=y
)
∧
(
3
y>6
))
。
对于
C
语言程序中的
skip
语句、
goto
语句和语句标号
,
在布尔程序中保持不变。
对于需要条件判断的语句
,
如
if
语句、
while
语句等
,
在布
尔程序中转变成结合3和
assume
语句的形式。例如
,if
语句
)
;
…
if
(
C
)
{
…
}else{
…
}
被转变为
if
(
3
)
{assume
(
C
′
}else
)
;
…
{assume
(
?
C
′
}
的形式
,if
(
3
)
不进行条件判断
,
由
as
2
sume
语句来进行。如果
C
恰好就是一个谓词
(
或谓词的非
)
,
那么
C
′就是
C
对应的布尔变量
(
或布尔变量的非
)
,
否则
C
′是
被
C
蕴涵的最强的谓词
(
或谓词的非
)
对应的布尔变量
(
或布
尔变量的非
)
。例如
,C=
(
y==3
)
,
谓词集合中不包含
(
y=
=3
)
这个谓词
,
但包含谓词
(
y<6
)
,
于是
C
′
={y<6}
。
SLAM
中的谓词抽象称为多态谓词抽象
[10]
。抽象一个
函数时
,
引入象征常量保存调用传入的实参值
,
在函数内涉及
到的实参值用象征常量代替
,
与具体的实参变量和实参值无
关
,
以此来建立与具体调用无关的抽象
,
使得对不同实参值的
调用都可以重用同一个抽象。谓词的作用域取决于谓词中变
量的作用域。包含全局变量的谓词是全局谓词
,
在抽象程序
的每条语句时都要考虑对全局谓词取值的影响
;
只包含某个
函数的局部变量的谓词是这个函数的局部谓词
,
只在抽象这
个函数时考虑对它取值的影响。对图
1
中的例子
,
抽象函数
inc
时只需考虑谓词集合
E
inc
={x==
′
x,x==
′
x+1,x<
4},
其中的谓词都是局部谓词。
C2BP
抽象
C
语言程序时
,
先生成每个函数的接口
,
然后
再抽象每个函数内的语句。假设函数
R
中只有一条返回语
句“
returnr;
”
,
函数
R
的接口是六元组
(
F
R
,r,S
R
,E
f
,E
r
,
B
R
)
。
F
R
是形参变量集合
,r
是函数的返回变量
,S
R
是象征常
量的集合。象征常量′
f
保存传递给形参变量
f
的实参值
,
图
1
(
b
)
布尔程序中的’
x
就是对应于
x
的象征常量
;
如果
f
是指
针
,
对于所有合法的3
k
f
(
k
∈
N,
3
k
表示
k
个3
)
,
引入象征
常量′3
k
f
保存函数开始时3
k
f
的值。
E
f
中包含的谓词是包
含形参变量而不包含
R
的局部变量和象征常量的谓词
,
称为
形参谓词。
E
r
中包含的谓词是包含返回变量或象征常量而
不包含除
r
以外任何局部变量和形参变量的谓词
,
称为返回
谓词。对于形参变量
f
和象征常量′
f,
在
R
的谓词集合中还
要加入谓词
(
f==
′
f
)
,
表示在函数开始时形参变量和象征常
量相等
,
这样的谓词称为绑定谓词
,
构成集合
B
R
。如果
f
是
・
256
・
指针
,
对于所有合法的3
k
f,B
R
中还包括绑定谓词
(
3
k
′
f=
=
′3
k
f
)
。绑定谓词对应的布尔变量在函数开始处被赋值为
true
。
BP
(
P,E
)
和一条带有特定标号的语句
s
error
,BEBOP
判定
s
error
在布尔程序中是否可到达。如果
s
error
可到达
,BEBOP
生成一
条从初始状态对应语句
s
0
到
s
error
的错误轨迹
,
代表抽象反例
路径。
BEBOP
的算法根据
RHS
[15,16]
算法修改而成。
BEBOP
根据
BP
(
P,E
)
构建一个控制流图
,
表示
BP
(
P,
E
)
的控制结构。控制流图的每个节点
v
对应于
BP
(
P,E
)
中
的一条语句
s
v
,v
的后继节点对应于
s
v
的后继语句。
BEBOP
从
s
0
对应的初始节点
v
0
开始为每个节点计算路径边
,
如果
一个节点对应于函数调用语句
,
则为它计算扼要边。
Ω
e
,
Ω
v
〉
对于节点
v,
它的一个路径边为〈
,s
e
是包含
s
v
的
函数的第一条语句
,
Ω
e
和
Ω
v
分别表示
s
e
和
s
v
执行前
BP
(
P,
E
)
中可见的布尔变量的取值情况。对于不在当前作用域内
的谓词
,
考虑它们的取值情况对验证没有意义
,
所以考虑可见
Ω
e
,
Ω
v
〉
布尔变量的取值情况就可以表示抽象状态。〈
表示存
在两段执行路径
,
一段从
s
0
到
s
e
,
另一段从
s
e
到
s
v
。本质上
v
的一个路径边代表了一种达到
s
v
的可能执行情况。
如果
v
对应于函数调用语句
,
那么它的一个扼要边为
Ω
1
,
Ω
2
〉
〈
,
Ω
1
和
Ω
2
分别表示被调函数执行前后调用函数中
可见布尔变量的取值情况。本质上
v
的一个扼要边代表了一
种可能的函数调用和相应的影响。
BEBOP
在计算路径边和扼要边时维持一个工作表
,
初始
其中只有
v
0
。每当为工作表中的一个节点
v
计算了一个路
径边
(
或扼要边
)
就把
v
从工作表中删除
,
然后根据
v
的路径
边
(
或扼要边
)
判断可以为
v
的哪些后继节点计算路径边
(
或
扼要边
)
,
等价于根据当前抽象状态判断在布尔程序中可以执
行哪些后继语句。把这些可以处理的节点加入工作表
,
继续
处理。如此这样不断扩展
,
有可能再次遇到
v,
这意味着一种
新的达到
s
v
的执行情况
,
需要为
v
计算新的路径边
(
或扼要
边
)
。
BEBOP
保存所有节点的路径边集合
(
或扼要边集合
)
。
如果算法结束时
s
error
对应节点
v
error
的路径边集合
(
或扼要边
集合
)
为空
,
则
s
error
是不可到达的
,P
满足被验证属性
,
结束验
证
;
否则
,s
error
是可到达的
,
生成错误轨迹。
BEBOP
生成从
s
0
到
s
error
的最短执行轨迹作为错误轨
迹
,
这条最短执行轨迹由对应的抽象反例路径上每条语句的
唯一编号和每条语句执行前可见布尔变量的取值情况组成。
为了找到最短执行轨迹
,
对于
v
的每个路径边
(
或扼要边
)
,
BEBOP
还保存对应的从
v
0
到
v
的路径长度
,
据此把路径边
集合
(
或扼要边集合
)
划分为不同的等价类。算法结束时可以
得知到达
v
error
的最短路径长度
,
然后从对应的等价类中任取
一个路径边
(
或扼要边
)
,
计算对应的轨迹。具体计算方法是
先生成
s
error
的编号和对应的可见布尔变量取值情况
,
然后寻
找
v
error
的一个前驱节点
u,u
的一个路径边
(
或扼要边
)
对应于
一条长度为
r-1
的路径
,
生成
u
对应语句的编号和可见布尔
变量取值情况
,
如此不断逆向处理
,
最终可以生成整条轨迹。
对于函数调用语句
v=R
(
a
1
,
…
,a
j
)
,
它的抽象分三步计
算
:
计算实参值
,
生成布尔程序中对应的调用
,
更新调用函数
布尔变量的取值。
首先
,C2BP
计算布尔程序中需要传递的实参值。因为
布尔程序中考虑的是对谓词取值的影响
,
所以布尔程序中的
形参变量是形参谓词对应的布尔变量
,
数量不一定等于形参
的数量。计算需要传递的实参值实际上是根据实参变量计算
形参谓词的取值。具体做法是把形参谓词中的形参变量替换
为实参变量
,
在调用函数中为每个这样得到的新谓词
α
i
引入
一个新的局部布尔变量
prm
i
来保存其真值
,
如果
α
i
(
或它的
非
)
在调用前被蕴涵
,
那么
prm
i
取值为
true
(
或
false
)
,
对应
的返回谓词的布尔变量在调用时被赋值为
prm
i
的值。例如
在图
1
(
b
)
中
,
语句“
prm=true;
”来源于根据实参变量
a
计算
出形参谓词
(
x<4
)
在调用前被蕴涵。
其次
,
生成布尔程序中的调用语句。为了反映被调函数
对调用函数中谓词取值的影响
,
布尔程序中被调函数返回的
不是
r
的值
,
而是所有返回谓词的取值情况
,
用于更新调用函
数中相关谓词的取值。具体做法是在被调函数中把“
return
φ
1
},
…
,{
φ
k
};
”
(
φ
i
为返回谓词
)
,
在调用
r;
”转变为“
return{
函数中为每个返回谓词
φ
i
引入一个新的局部布尔变量
ret
i
来保存其真值。这样
,
在布尔程序中函数调用语句被转换为
ret
1
,
…
,ret
k
=R
(
prm
1
,
…
,prm
n
)
的形式。
最后
,
更新调用函数中相关谓词的取值。在调用函数中
,
所有包含
v
的谓词都需要被更新。一些全局变量可能被
R
更改
,
所以所有包含这些全局变量的谓词也需要被更新。因
为调用函数中可能有指针指向
v
或全局变量
,
所以包含这些
指针的谓词也需要被更新。另外
,
调用时可能传递指向调用
函数局部变量的指针
,
那么这些局部变量也可能被更改
,
所以
相关谓词也需要被更新。
C2BP
使用可能别名分析
[12]
来生成
需要更新的谓词集合的上近似。更新的具体做法是把返回谓
词中出现的
r
替换为
v,
象征常量′
f
替换为对应的实参变量
kk
a
i
,
′3
f
替换为3
a
i
,
这样返回谓词就被翻译成了调用函数
中的形式
,
然后结合调用函数中原有的谓词取值情况
,
判断哪
些新的取值情况被蕴涵
,
据此来更新相关布尔变量的取值。
这样
,
一个
C
语言程序
P
就被转化为对应的布尔程序
BP
(
P,E
)
,BP
(
P,E
)
反映了
P
中每条语句的执行对谓词取值
的影响
,
即对某些共性的影响。在
BP
(
P,E
)
的某一点
,
这些
影响的累积就是
P
的抽象状态
,
这些影响就是抽象状态的转
换关系。因为可以根据
BP
(
P,E
)
得到
P
的抽象状态和抽象
状态的转换关系
,
所以可以生成
P
的抽象状态转换路径
,
对
P
进行验证。
3
验证
验证的过程就是判定状态转换路径是否满足特定要求的
过程。
SLAM
和
BLAST
利用判定一条带有特定标号的语句
在抽象状态转换路径中是否可到达来实现软件时态安全性属
性的验证
[13,4]
。如果从程序的一个初始状态开始最终可以执
行某条语句
,
则这条语句是可到达的。如果到达某条语句意
味着破坏被验证属性
,
则可以根据这条语句是否可到达来判
定被验证属性是否成立。
BEBOP
[13,14]
是
SLAM
中的模型检测器。对于布尔程序
4
细化
对于一条抽象反例路径
,
如果对应的具体路径是可行的
,
则意味着找到了一个真正的系统错误。但是
,
由于抽象模型
比具体系统粗糙
,
所以有可能引入虚假反例路径。例如在第
2
节中曾提到
,
程序
P
中的条件
(
y==3
)
在布尔程序
BP
(
P,
E
)
中被抽象为
(
y<6
)
,
这样就使得在
BP
(
P,E
)
中本来只有在
(
y==3
)
时才能执行的语句在其他一些情况下也可以执行
,
可能导致出现
P
中不会出现的错误。虚假反例路径对应于
具体系统中的不可行执行路径。如果经判定反例路径是虚假
・
257
・
的
,
则应该把它从抽象模型中排除
,
但是根据当前信息进行抽
象得到的抽象模型必然导致这条虚假反例路径的出现
,
所以
必须适当的增加信息
,
使得可以抽象出更加精细的排除了这
条虚假反例路径的抽象模型。这些用于排除虚假反例路径的
信息是通过对不可行路径进行分析而得到的
,
所以这种细化
被称为反例驱动的细化
[17,18,13,19]
。
SLAM
中用工具
NEWTON
来进行反例驱动的细化
[20]
。
如果错误轨迹对应的具体反例路径
p
是可行的
,
则输出这条
错误轨迹
,
指示一个真正的错误
;
如果
p
不可行
,
则这个反例
是虚假的
,
生成用于排除虚假反例路径的谓词
,
添加到谓词抽
象的谓词集合中。即使谓词抽象的初始谓词集合为空
,
NEWTON
也会找到验证所需的足够谓词
,
所以
SLAM
不需
要人为提供辅助信息。
NEWTON
把
p
预处理为只包含赋值语句、
assume
语句、
函数调用语句和返回语句的等价路径
p
′。具体反例路径是
程序
P
中被执行的语句的序列
,
等价于一个顺序语句序列。
在路径中
,skip
可以省略
;goto
语句转向的语句就在
goto
语
句之后
,
所以
goto
语句也可以省略
;
对于需要条件判断的语
句
,
由于具体反例路径已经表明在执行时作了什么判断
,
所以
只保留这种判断对应的
assume
语句即可
;
除函数调用语句以
外影响变量取值
(
即影响系统状态
)
的语句等价于赋值语句
,
所以可以替换为赋值语句。因此
,
经过这样预处理得到的路
径
p
′与原来的具体反例路径
p
对系统状态的影响是等价的。
模型检测关注的是系统的状态和状态的转变
,
所以可以用
p
′
代表
p
。
在程序
P
中
,
正是条件判断决定了语句执行的方向
,
决
定了是否能执行导致错误出现的语句块
,
而在一个语句块中
,
语句只是被顺序执行而已。所以
,
如果一条具体反例路径是
可行的
,
那么路径中所有条件判断做出的选择都应该是符合
条件的合理选择
;
如果具体反例路径不可行
,
必然在验证时做
出了在
BP
(
P,E
)
中符合条件而在
P
中不符合条件的不合理
选择
,
导致执行了不该执行的语句。对于
p
′
,NEWTON
参考
变量的取值情况构建一个表示
p
中条件判断做出的选择的公
式
e,p
是否可行对应于
e
是否可满足。对于不可行路径
,
NEWTON
计算它的解释
,
用于生成排除对应虚假路径的谓
词。
NEWTON
用象征常量代表变量的取值。当
p
′中语句
s
i
最先使用一个变量
x
的值并且没有任何象征常量可以表示
x
的值的时候
,NEWTON
引入一个象征
θ
x
来代表
x
的值
,
并在
s
i
前插入语句“
x=
θ
,
这样的语句被称为注释
;
对于可以根
x
;
”
据其他变量的值来确定取值的变量
,
用相关的象征常量表式
它们的取值。
p
′中用
assume
语句来表示条件判断做出的选
择
,
如果某条
assume
语句的条件根据条件中变量的取值情况
被前面所有
assume
语句的条件的合取所蕴涵
,
则为这个条件
中没有自己的象征常量的变量引入新的象征常量
,
并在这条
assume
语句前插入新的注释
,
利用象征常量的差异消除蕴
涵
,
使得这个条件在构建公式
e
时也有意义。在调用函数时
,
为了避免用实参的象征常量表示被调函数中变量的取值
,
与
谓词抽象中一样
,
为每个形参引入一个象征常量
,
其值等于实
参值。对于指针
,
除了引入象征常量表式指针的值
,
还引入象
征常量表式可以根据指针访问的值。
语境是三元组〈
Ω
,
Φ
,
∏〉
,
其中
Ω
是一条语句执行前各
变量用象征常量表示的取值情况的集合
,
称为存储
;
Φ
是用象
征常量表示的所有
assume
语句的条件的集合
,
称为条件
;
∏
是各个变量曾经的取值的集合
,
称为历史。
NEWTON
的具体做法是把语境作为最强后置条件
,
在
p
′的起点以空语境开始不断计算新的语境。对于除
assume
语句外的语句
,
更新
Ω
和∏
;
对于
assume
语句
,
更新
Φ
。在更
新时
,
还要标出
Ω
和
Φ
中的元素依赖
Ω
和∏中的哪些元素。
∧
Φ
c
就是公式
e
。如果处理了某条
assume
语句后出现
c
∈
∧如果
p
是可行
Φ
c
不可满足的情况
,
则路径是不可行的。
c
∈
的
,
则根据变量的取值情况
p
中所有条件判断做出的选择都
是符合条件的
,
此时公式
e
根据变量的取值情况是可满足的
;
如果
p
不可行
,
则根据变量的取值情况
p
中有的条件判断做
出的选择不符合条件
,
此时公式
e
根据变量的取值情况是不
可满足的。不符合条件的选择来源于抽象模型没有关注某些
信息
,
如果关注了必要的信息就不会做出不符合条件的选择。
例如
,p
′为语句序列“
x=
θ
x
;y=2x;assume
(
y=x
)
;ER
2
θθ
ROR:;
”
,
表示
(
y=x
)
的公式
c
为
(
x
=2
x
)
,
显然
e
不可满足
,
如果在抽象时关注了
y
是否等于
x,
那么在验证时就不会认
为
(
y=x
)
的分支可以执行。当
e
不可满足时
,NEWTON
从
Φ
中删除一个条件
,
如果∧
Φ
c
仍旧不可满足
,
则这个条件与虚
c
∈
假反例无关
,
可以被忽略
;
否则
,
保留这个条件。这样不断处
理
,
会得到最小的解释
p
不可行的
Φ
,
表示不符合条件的选择
和相关的选择
,
如果谓词抽象时考虑这些信息就可以排除这
条虚假反例路径。根据
Ω
和
Φ
中元素与
Ω
和∏中元素的依
赖关系和插入的注释
,
可以把最小
Φ
中的条件转换为变量表
示的形式
,
这就是谓词抽象需要增加的谓词。
把这些谓词加入谓词集合
E,
根据新的谓词集合进行抽
象
,
因为考虑了新增谓词的取值情况
,
所以抽象模型中不包含
这条虚假反例路径
,
在验证阶段不会走向这条虚假反例路径。
例如对上段中的例子
,
在谓词集合中加入谓词
(
y=x
)
,
对语句
“
y=2x;
”进行谓词抽象后布尔变量
{y=x}
的值为
false,
这就
排除了转入
(
y=x
)
为
true
的分支的可能性
,
在验证时不会因
为执行了只有在
(
y=x
)
为
true
时才能执行的语句而导致错
误出现。
如此这样按照抽象2验证2细化的范例继续进行
,
就可以
继续验证程序
P
是否真正满足被验证属性。
5
BLAST
抽象2验证2细化这三步循环在步骤
1
和步骤
2
都是计算
难题。
BLAST
采用被称作
lazyabstraction
的方法
,
集成并优
化了这三步循环
,
极大的提升了性能
[4]
。
Lazyabstraction
的
思想是由验证驱动
,
不断按需求抽象和细化一个抽象模型
,
把
抽象、验证和细化结合在一起进行。因为对程序的某一点只
按需求细化到足够的精度
,
所以模型的不同部分有不同的精
度。
BLAST
把每个函数预处理为控制流自动机。自动机的
节点代表程序的特定位置
,
自动机的边被标上由若干条语句
组成的程序片断或条件判断的条件的真值
,
表示如何从一个
位置执行到另一个位置。
然后
,BLAST
根据各个控制流自动机和谓词集合从程序
的初始位置出发
,
深度优先的计算程序在各个位置的抽象状
态
,
建立一棵搜索树
,
判断是否能执行意味着错误的语句
,
达
到错误状态。搜索树的节点对应于抽象状态
,
标有一个谓词
集合和其中谓词的布尔组合
,
谓词集合表示在此处关注的事
实和抽象精度
,
布尔组合表示此处的抽象状态。
抽象状态的计算是根据一个谓词的最弱前置条件在前一
・
258
・
个状态是否被蕴涵来判断这个谓词在当前的取值。计算了一
个抽象状态后
,
根据这个抽象状态判断搜索树可以如何扩展
,
扩展搜索树并为扩展出的节点计算抽象状态。这样边计算抽
象状态边搜索即是同时进行抽象与验证。如果一个节点的抽
象状态是所有访问过节点的抽象状态集合的子集
,
这个节点
称为被覆盖节点
,
可以在这个节点停止继续搜索
,
因为从这个
节点可以进行的扩展在前面的节点也可以进行。每当遇到被
覆盖节点就回溯
,
按深度优先顺序选择没有扩展的分支继续
搜索。如果达到了错误状态
,
则转入细化阶段
,
否则
,
当搜索
树无法再扩展时就找到了所有可到达的状态
,
可以认定程序
没有错误。
如果在构建搜索树时达到了错误状态
,
那么在搜索树的
根节点到错误状态节点的路径上的语句就构成了具体反例路
径。为了判定这条路径是否可行
,
构建一个路径公式
,
具体反
例路径是否可行对应于路径公式是否可满足。为了构建路径
公式
,
要为每条语句生成变量值的约束
,
表示每条语句对变量
值的影响。
BLAST
也用赋值语句、
assume
语句、函数调用语
句和返回语句来表示路径
,
所以只为这四种语句生成约束。
赋值语句的约束是把赋值语句中的变量
x
替换为常量〈
x,i
〉
,
其中
i
是
x
的不同取值的编号。如果
x
是指针变量
,
用〈3
〈
x,i
〉
,j
〉表示3
x
。生成包含指针变量的约束时可能还要生成
关于指针的间接引用的约束
,
一条语句的所有约束用合取符
号连接。
assume
语句的约束就是它的条件
,
其中的变量也作
替换。对于函数调用语句
,
引入象征常量代表实参值
,
函数调
用语句的约束是把实参值赋值给象征常量的约束
,
并且认为
在被调函数的第一条语句前存在
assume
语句
,
其条件就是形
参变量等于象征常量。调用函数时遇到的指针变量用与
SLAM
类似的方法处理。返回语句的约束是把返回值赋值
给调用函数中获取返回值的变量的约束。具体反例路径上所
有约束的合取就是路径公式
,
如果具体反例路径是可行的
,
则
根据变量的取值在条件判断时做出的选择是合理的
,
路径公
式是可满足的。
如果路径公式不可满足
,BLAST
应用克雷格插值来计算
排除这条虚假反例路径所需的谓词
,
然后在搜索树中重新扩
展这条路径
[21]
。子句集
A
和
B
的克雷格插值式
[22]
是满足如
下要求的公式<
:
(
1
)
A
蕴涵<
;
(
2
)
<与
B
不一致
;
(
3
)
<只包含
A
和
B
的公共变量。可以从
A
和
B
不一致的归结证明在线
性时间内生成
A
和
B
的克雷格插值式
[23]
。
把路径公式以某个抽象状态为界分成分别表示前后两段
路径的子句集
A
和
B,
由此得到的克雷格插值式<被
A
蕴
涵
,
而且由
A
和
B
的公共变量构成
,
所以<表示的是分割点
处具体状态集合的上近似
,
即前半段路径的可到达状态的上
近似
,
又因为<与
B
不一致
,
所以从<表示的状态出发无法执
行后半段路径的所有语句
,
达到错误状态。把<翻译成若干
谓词
,
加入分割点处的谓词集合
,
在重新扩展这一点时根据新
的谓词集合计算抽象状态
,
再根据得到的抽象状态决定如何
继续扩展。由于原有谓词集合可能为空
,
也可能不为空
,
所以
新的抽象状态表示的具体状态集合可能等于<表示的具体状
态集合
,
也可能是它的子集
,
但从其中的任何状态出发都无法
执行后半段路径。在具体反例路径上每个抽象状态的位置都
这样计算克雷格插值式并用获得的谓词补充该处的谓词集
合
,
则在重新扩展这条路径时必然在某一点转向其他方向。
BLAST
边抽象边验证
,
且只抽象到能够排除虚假反例的
精度为止
,
这样就避免了独立的代价高昂的抽象模型构建阶
段。另外
,BLAST
只对抽象模型的当前部分进行验证
,
这样
就避免了对无关部分进行不必要的搜索。所以
,BLAST
减低
了抽象和验证阶段的计算困难。根据克雷格插值式为某一点
得到的谓词只对这一点有意义
,
在其他地方不必考虑这些谓
词
,
所以每个抽象状态都有自己的谓词集合
,
这样就避免了考
虑无关谓词的取值所花费的巨大代价。
6
相关工作
MAGIC
是另一个基于抽象2验证2细化范例的软件模型
检测工具
,
使用了组合推理
,
用于验证组件的规格说明和
C
语言实现是否一致
[24]
。
MAGIC
把程序抽象为
LTS
(
labeled
transitionsystems
)
M
Imp
,
然后验证描述规格说明的
LTS
M
Spec
是否是
M
Imp
的安全抽象。如果答案是肯定的
,
则程序满
足属性
,
验证结束
;
否则
,
判断反例是否是真实的
,
如果反例是
虚假的
,
则计算一个改进的
M
Imp
,
继续验证。
ESC/Java
是使
用谓词抽象验证
Java
程序的模型检测工具
[25,26]
,
它把
Java
程序和规格说明翻译为称作验证条件的逻辑公式
,
根据验证
条件是否可满足来判定程序是否正确
,
由于抽象的原因
ESC/
Java
可能报告虚假反例。
Visser
等人描述了用于
C
++
的谓
词抽象技术及用于
Java
语言的实现
[7]
,
抽象的结果是新的
Java
程序
,
其中去掉了一些变量
,
加入了一些表示谓词取值情
况的布尔变量。这个新的
Java
程序可以用
JavaPathFind
2
er
[27]
进行验证。
Bandera
是另一个
Java
程序抽象工具
[28,29]
,
它根据用户的规格说明对程序进行切片
,
去除无关的部分
,
然
后对程序进行数据抽象
,
把得到的结果翻译为某些现有模型
检测工具的输入。
结论 在诸多验证方法中
,
模型检测因为高度自动化、对
使用者要求不高、覆盖系统全部状态和可以生成反例等原因
而受到越来越多的关注。本文以
SLAM
和
BLAST
为例介绍
了基于抽象2验证2细化范例的软件模型检测。目前软件模型
检测还处在起步阶段
,
距离真正成熟还有许多工作要做。
参考文献
1BallT,ticallyvalidatingtemporalsafety
8thInternationalSPINWorkshopon
ModelCheckingofSoftware,Toronto,Canada,2001
2ClarkeE,GrumbergO,JhaS,rexample
2
guidedab
2
13thConferenceonComputerAided
Verification,Chicago,USA,2000
7th
InternationalStaticAnalysisSymposium,SantaBarbara,USA,
2000
HenzingerTA,JhalaR,MajumdarR,straction.
The29thAnnualACMSIGPLAN
2
SIGACTSymposiumonPrin
2
ciplesofProgrammingLanguages,Portland,USA,2002
5GrafS,uctionofabstractstategraphswithPVS.
The10thConferenceonComputerAidedVerification,Haifa,Is
2
rael,1997
DasS,DillDL,encewithpredicateabstraction.
The12thConferenceonComputerAidedVerification,Trento,
Italy,1999
7VisserW,ParkS,redicateabstractiontoreduce
object
2
3rdWorkshop
8
onFormalMethodsinSoftwarePractice,Portland,USA,2000
BallT,MajumdarR,MillsteinT,ticpredicateab
2
2001ACMSIGPLANConference
onProgrammingLanguageDesignandImplementation,Snow
2
bird,USA,2001
4
6
・
259
・
9FlanaganC,ateabstractionforsoftwareverifi
2
29thAnnualACMSIGPLAN
2
SIGACTSymposium
andAlgorithmsforConstructionandAnalysisofSystems,Geno
2
va,Italy,2001
20BallT,tingabstractexplanationsofspuri
2
ouscounterexamplesinCprograms:[TechnicalReport].Red
2
mond,USA:MicrosoftResearch,2002
21HenzingerTA,JhalaR,MajumdarR,ctionsfrom
31stACMSIGPLAN
2
SIGACTSymposiumonPrin
2
ciplesofProgrammingLanguages,Venice,Italy,2004
reasoning:AnewformoftheHerbrand
2
Gentzen
lofSymbolicLogic,1957,22
(
3
)
:250
～
268
23Pudl
á
oundsforresolutionandcuttingplaneproofs
lofSymbolicLogic,1997,62
(
2
)
:981
～
998
24ChakiS,ClarkeE,GroceA,rVerificationofSoft
2
nsactionsonSoftwareEngineer
2
ing,2004,30
(
6
)
:388
～
402
25FlanaganC,LeinoKRM,LillibridgeM,edstatic
2002ACMSIGPLANConferenceonPro
2
grammingLanguageDesignandImplementation,Berlin,Germa
2
ny,2002
26FlanaganC,ateabstractionforsoftwareverifi
2
29thAnnualACMSIGPLAN
2
SIGACTSymposium
onPrinciplesofProgrammingLanguages,Portland,USA,2002
27HavelundK,heckingJavaprogramsu
2
ationalJournalonSoftwareToolsfor
TechnologyTransfer,2000,2
(
4
)
:366
～
381
28CorbettJ,DwyerM,HatcliffJ,a:Extractingfi
2
nite
2
22ndInternational
ConferenceonSoftwareEngineering,Limerick,Ireland,2000
29DwyerM,HatcliffJ,JoehanesR,
2
supportedprogram
abstractionforfinite
2
23ndInternational
ConferenceonSoftwareEngineering,Toronto,Canada,2001
onPrinciplesofProgrammingLanguages,Portland,USA,2002
10BallT,MillsteinT,rphicpredicateab
2
nsactionsonProgrammingLanguagesand
Systems,2005,27
(
2
)
:314
～
343
11BallT,nprograms:Amodelandprocess
forsoftwareanalysis:[TechnicalReport].Redmond,USA:Mi
2
crosoftResearch,2000
ation
2
basedpointeranalysiswithdirectionalassign
2
2000ACMSIGPLANConferenceonProgramming
LanguageDesignandImplementation,Vancouver,Canada,2000
13BallT,:Asymbolicmodelcheckerfor
7thInternationalSPINWorkshopon
ModelCheckingofSoftware,Stanford,USA,2000
14BallT,:Apath
2
sensitiveinterprocedural
2001ACMSIGPLAN
2
SIGSOFTWorkshop
onProgramAnalysisforSoftwareToolsandEngineering,Snow
2
bird,USA,2001
15RepsT,HorwitzS,einterproceduraldataflowa
2
22ndACMSIGPLAN
2
SI
2
GACTSymposiumonPrinciplesofProgrammingLanguages,San
Francisco,USA,1995
16RepsT,HorwitzS,einterproceduraldataflowa
2
tical
ComputerScience,1996,167:131
～
170
er
2
aidedVerificationofCoordinating
ton,USA:PrincetonUniversityPress,1994
18RusuV,ingsafetypropertiesbyintegra
2
tingstaticanalysis,5thIn
2
ternationalConferenceonToolsandAlgorithmsfortheConstruc
2
tionandAnalysisofSystems,Amsterdam,theNetherlands,
1999
19LakhnechY,BensalemS,BerezinS,entalverifica
2
7thInternationalConferenceonTools
(
上接第
188
页
)
之后的研究论文中逐一讨论。
下
,
发现基于实例特征的位于不同
Ontology
分类树的两个概
念对的相似性
,
同时判断一个概念在另一个
ontology
中的相
对位置
,
获取基于实例特征的概念相似性矩阵及位置特征矩
阵。
匹配标记器
(
如
:HiddenMarkovModelLabeler
)
在分析
树结构、领域公理约束、共有知识的基础上
,
利用概念相似性
矩阵及位置特征矩阵标记映射关系
,
获得参考匹配结果。
利用概念相容性检测、实例一致性检测推理机
(
如
:Tab
2
leauAlgorithms
)
检测参考匹配结果
,
最后获得可以信赖的结
果。当然
,
半自动方式下进行的有条件映射标记
,
也是可以接
受的
(
如
:ProtegePROMPT
)
。
总结 语义服务是下一代
WebWeb
服务必须解决的难
点问题
,
语义网为实现广泛的语义服务提供了可能
,Ontology
是语义网体系结构的核心。分布式协作系统的重要问题是本
体的匹配和集成
,
针对协作的分布式系统需要语义互联的问
题
,
本文分析了造成语义互联困难的主要因素是本体的匹配
和集成
,
提出了一个基于机器学习的
Ontology
集成的框架模
型。该框架的四个关键步骤是
:
学习分类算法及策略、相似性
评估、标记算法、相容性一致性检测。
基于机器学习的本体概念匹配研究才刚刚起步
,
本文提
出的这个框架
,
结构完整
,
每一步工作的目标明确
,
我们将在
参考文献
1
2
Berners
2
LeeT,HendlerJ,anticWeb,Scien
2
tificAmerican,2001,284
(
5
)
:34
～
43
FosterI,KesselmanC,NickJM,siologyofthe
Grid
2
AnOpenGridServicesArchitectureforDistributedSys
2
:///ogsa/,Feb.2002
WeNeedforOntologyIntegrationontheSe
2
manticWeb,:orkshopon
SemanticIntegration,the2ndInternationalSemanticWebCon
2
ference,SanibalIsland,Florida,USA,Oct.2003
StuderR,BenjaminsVR,dgeEngineering,
dKnowledgeEngineering,1998
,25
(
122
)
:161
～
197
JurisicaI,MylopoulosJ,giesforKnowledgeMan
2
agement:dgeand
InformationSystems,2004,6
(
4
)
:380
～
401
BaaderF,McGuinnessD,NardiD,crip
2
tionlogichandbook:theory,implementationandapplications
[Z].Cambridge:CambridgeUniversityPress,2002
NaingMyo
2
Myo,LimyEe
2
Peng,Hoe
2
gy
2
:
ProceedingsoftheThirdInternationalConferenceonWebInfor
2
mationSystemsEngineering
(
WISE
)
,Singapore,2002
李善平
,
尹奇
,
胡玉杰
,
等
.
本体论研究综述
.
计算机研究与发展
,
2004,41
(
7
)
3
4
5
6
7
8
・
260
・
发布评论