第8讲 模型检测

软件测试技术白盒测试和黑盒测试静态测试和动态测试（验证测试和确认测试）传统测试方法和面向对象测试的方法静态方法直接检查源代码或其它文档同行评审桌面检查代码审查走查软件验证同行评审也称好友评审不是很正式：“你把你的拿给我看看，我把我的拿给你看看”由软件设计和编码人员加上一两个其它程序员或测试人员组成桌面检查对源程序代码进行人工分析、检验关注变量值和程序逻辑记录检查结果最好由非程序作者本人模拟执行程序只有一个人在阅读代码，没有团队协作桌面检查5示例审查(Inspection)软件业最佳实践重点放在查找工作产品缺陷上文档必须通过质量关卡（核对表，Checklist）审查(Inspection)角色主持人：控制进度，分派和跟踪任务，报告审查结果作者：陈述项目的概况，解释代码中不清晰的部分评论员：找缺陷，不讨论解决方案记录员：记录发现的错误，以及指派的任务代码走查走查小组与代码审查类似，但检查方法不同测试者准备代表性的测试用例与会者“充当”计算机，人工运行用例许多错误在提问的过程中被发现9软件验证验证系统的正确性安全攸关系统、任务关键系统分类基于证明的验证模型检测（ModelChecking）10基于证明的验证系统：逻辑公式集合Γ规约：公式

验证：Γ├

，即：Γ可推导出一般需要用户引导和专门知识1980’s早期由Clarke和Emerson

，Queille和Sifakis

独立开发模型检测2007年图灵奖获得者开发模型检测技术，并使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术所做的奠基性贡献。12模型检测M模型检验器p→Fqyesnoφ反例自动的、基于模型的、性质验证方法系统：有穷状态模型M（Kripke结构）规约/性质：时序逻辑验证：M╞，即：M是否满足

13Kripke结构3元组M=(S,T,L)

S：有穷状态集T

SS：状态迁移关系，满足

sS,s’

S

(s,s’)

TL：S2AP：状态标记函数。其中， AP为原子命题集，L(s)表示状态s中为真的原子命题集14Kripke结构AP：{p,q,r}S:{s0,s1,s2}T:{(s0,s1)

,(s1,s1),(s2,s1),(s2,s0),(s0,s2)

}L(s0)={p,q}L(s1)={q}L(s2)={q,r}p,qq,rqs0s1s2示例Kripke结构16Kripke结构路径（path）一个无穷状态序列：=<s1,s2,s3,…>, i

1(si,si+1）T路径也表示为：s1→s2

→s3

→…i

：从si开始的后缀。如：

3：

s3→s4→…17Kripke结构p,qq,rqs0s1s2p,qp,qs0q,rs2qs1qs1qs1s0qs1qs1q,rs2qs1路径计算树18时序逻辑模型检测回顾系统：有穷状态模型M（Kripke结构）规约/性质：时序逻辑验证：M╞，即：M是否满足

在模型中，性质公式的真值不是静态的，当系统从一个状态到另一个状态时，公式的真值会变化。19时序逻辑线性时间逻辑时间为路径集合分支时间逻辑时间表示为“树”20线性时序逻辑LTLAmirPnueli(1941-2009)TheWeizmannInstituteofScience1996年图灵奖获得者把时态逻辑引入计算机科学的开创性工作，以及在编程语言和系统验证方面的突出贡献21LTLLTL:Linear-timeTemporalLogic语法::=|T|p| ()|()|()|()|

X|G|F|

U

其中，p为原子命题，为LTL公式22LTL时序操作符X：下一状态（neXt）F：某个将来（

Future）状态G：所有（Globally）将来状态U：直到（Until）23LTL优先级一元操作（¬、X、F、G）两元时序操作（U、R、W）逻辑运算符（、）逻辑运算符（）例如

F(p→Gr)

¬qUp=

(F(p→(Gr))

((¬q)

Up))

a

a

在当前状态为真LTL的形式语义a…

a

a

在当前状态为真

Xa

a在下一个状态为真LTL的形式语义a…

a

a

在当前状态为真

Xa

a在下一个状态为真

Fa

a在将来的某个状态为真LTL的形式语义…a…LTL的形式语义

aa

在当前状态为真

Xa

a在下一个状态为真

Fa

a

在将来的某个状态为真

Ga

a

在将来的所有状态为真aaaaa…LTL的形式语义aa…ab

a

a

在当前状态为真

Xa

a在下一个状态为真

Fa

a

在将来的某个状态为真

Ga

a

在将来的所有状态为真

aUb

a

为真直到

b变为真29LTL的形式语义设：M

=(S,T,L)，

=s1→s2→

…

|=T,|≠

|=a

iff

a

L(s1)

|=

iff

|≠

|=12

iff

|=1

|=2|=12

iff

|=1

|=2|=12

iff

|=

1|=230LTL的形式语义

|=X

iff

2|=

|=G

iffi1i|=

|=F

iffi1i|=

|=1U2

iff(i1i|=

2) (j[1,i)

j|=

1)31LTL的形式语义设模型

M

=(S,T,L)，s

S，φ为LTL公式，则：M,s|=φ，如果从s开始的每一条路径，

|=φ32示例M,s0

|=

X

q

M,s0|=

G(pr)M,s1

|=

G

qM,s0

|=

p

U

qp,qp,qs0q,rs2qs1qs1q,rs2s0p,qq,rs2s0qs1q,rs2qs133实例不可能到达一个状态：started成立ready不成立 G(startedready)如果一个请求发生，它最终会被确认 G

(requested→F

acknowledged)如果进程不时地（infinitelyoften）被使能，那么就会不时地运行 GF

enabled

GF

running乘客要到5楼，2楼的向上电梯不会改变运行方向 G(f2upp5→(upUf5))34LTL公式的等价Gφ

≡

F

φ

，Fφ

≡

G

φXφ

≡

X

φFφ

≡

T

U

φ，Gφ≡R

φφ

W

≡R(φ

)φR

≡W(φ

)分配律F(φ

)≡FφF，但F(φ

)FφFG(φ)≡Gφ

G，但G(φ)Gφ

GLTL的表达能力互斥安全性(safety)：坏事永不发生

任何时候只有一个进程处于临界区活性(liveness)：好事总会发生

只要请求进入临界区，会被允许进入无阻性(non-blocking)

进程总可以请求进入临界区非严格顺序性

无需按严格顺序进入临界区LTL的表达能力两个进程：ntcn…n：处于非临界状态t：试图进入状态c：处于临界状态s0n1n2s3s2s1t1n2c1n2t1t2c1t2s4s6s5n1t2n1c2t1c2s7LTL的表达能力安全性：G(c1

c2)所有状态满足安全性s0n1n2s3s2s1t1n2c1n2t1t2c1t2s4s6s5n1t2n1c2t1c2s7LTL的表达能力活性：G(t1

Fc1)

s0n1n2s3s2s1t1n2c1n2t1t2c1t2s4s6s5n1t2n1c2t1c2s7不满足LTL的表达能力无阻性

对所有满足n1的状态，存在路径进入满足t1

的状态s0n1n2s3s2s1t1n2c1n2t1t2c1t2s4s6s5n1t2n1c2t1c2s7表达不了LTL的表达能力非严格顺序性存在路径，两个满足c1的状态的中间状态都不满足c1和c2s0n1n2s3s2s1t1n2c1n2t1t2c1t2s4s6s5n1t2n1c2t1c2s7表达不了LTL的表达能力重新建模n1n2s3s2s1t1n2c1n2t1t2c1t2s4s0s6s8s5n1t2t1t2n1c2t1c2s7s0n1n2s3s2s1t1n2c1n2t1t2c1t2s4s6s5n1t2n1c2t1c2s7G(t1

Fc1)42计算树逻辑CTL(Computationaltreelogic)语法

::=|T|p| ()|()|()|()|

AX|EX|AG|EG|AF|EF

|

A[

U]|E[

U]

其中，p为原子命题，为CTL公式43时序逻辑操作符

AX,EX,AG,EG,AU,AF,EFA：所有（

All）路径inevitablyE：存在

（Exists）一条路径possiblyX：下一状态（neXt）F：某个将来（

Future）状态G：所有（Globally）将来状态U：直到（Until）44时序逻辑操作符优先级一元运算符：,AG,EG,AF,EF,AX,EX,,AU,EU45时序逻辑操作符

EG

rAG(q

EGr)A[p

U

EFr]EFEGp

AF

r

EF(r

U

q)AF[(r

U

q)(p

U

r)]CTL:示例EFg

gCTL:示例AFg

gggCTL:示例AGggggggggCTL:示例EGg

ggg50CTL的形式语义设模型M

=(S,T,L),路径集Path(M)M,s|=T,M,s|≠,s

∈SM,s

|=p

iff

p

∈L(s)M,s

|=

iff

M,s

|≠

M,s|=12

iff

M,s|=1

M,s|=2M,s|=12

iff

M,s|=1

M,s|=2M,s|=12

iff

M,s|≠

1

M,s|=251CTL的形式语义M,s|=AX

iff

(s,s’)T,M,s’|=

M,s|=EX

iff(s,s’)T,M,s’|=

M,s|=AG

iff

<s1,s2,…>Path(M),s=s1,i1M,si|=

M,s|=EG

iff

<s1,s2,…>Path(M),s=s1,i1M,si|=

52CTL的形式语义M,s|=AF

iff

<s1,s2,…>Path(M),s=s1,

i1M,si|=

M,s|=EF

iff

<s1,s2,…>Path(M),s=s1,

i1M,si|=

M,s|=A[1U2]iff

<s1,s2,…>Path(M),s=s1,

i1M,si|=

2

j<iM,sj|=

1

M,s|=E[1U2]iff<s1,s2,…>Path(M),s=s1,

i1M,si|=

2

j<iM,sj|=

1

53实例1)不可能到达一个状态：started成立ready不成立2)可能到达一个状态：started成立ready不成立3)如果一个请求发生，它最终会被确认4)乘客要到5楼，2楼的向上电梯不会改变运行方向

CTLLTL1)AG(startedready)G(startedready)2)EF

(startedready)3)AG

(requested→AF

acknowledged)G

(requested→F

acknowledged)4)AG(f2upp5→

A(upUf5))G(f2upp5→(upUf5))LTL与CTL的比较直观比较CTL较强LTL不能表达：任何状态可以到达restart状态CTL表达：AGEFrestartLTL较强LTL可以描述在所有路径上选择一个范围F

p

F

q：每条有p的路径，也有qAFp

AFq和AG(p

AFq)含义都与之不同CTL的模型检验算法给定M

=(S,T,L),s0S和，计算M,s0|=

若M不满足，产生反例CTL的一个时态连接词集合是充分的，当且仅当它至少包含{AX,EX}中之一，{EG,AF,AU}中之一以及EU只考虑：{,,}和{AF,EU,EX}CTL的模型检验算法算法原理方法1输入：M,s0和输出：yes或no方法2输入：M和输出：满足的状态集，检查s0是否在该集合CTL的模型检验算法标记算法SAT()输入：M和

输出：满足

的状态集合步骤转换

//只包含{,,}和{AF,EU,EX}从中的原子命题开始直到，对每个子公式，用标记使它满足的所有状态输出有标记的所有状态CTL的模型检验算法计算能标记状态：没有任何状态能带标记p：若p

L(s)，则s

带标记p12：如果状态s

同时带标记1和2，则可用12标记s1：如果状态s不带1，则可标记1CTL的模型检验算法AF 1、状态s

带，则可标记AF 2、若状态s的所有后继状态带AF，则可用AF标记s。重复该过程，直到标记无变化AFAFAF…AFAFAF…CTL的模型检验算法EX 如果状态s有一个后继状态带，则s可标记EX…EX

…CTL的模型检验算法E[1U2]

1、状态s

带2，则可标记E[1U2] 2、重复：若状态s带1并且至少一个后继状态带E[1U2],则s可标记E[1U2]1E[1U2]…1E[1U2]E[1U2]…2E[1U2]CTL的模型检验算法示例：互斥模型，E[c2

Uc1]是否满足？n1n2s3s2s1t1n2c1n2t1t2c1t2s4s0s6s8s5n1t2t1t2n1c2t1c2s7CTL的模型检验算法1,标记c1n1n2s3s2s1t1n2c1

n2t1t2c1

t2s4s0s6s8s5n1t2t1t2n1c2t1c2s7CTL的模型检验算法2,标记c2n1n2c2s3s2s1t1n2c2c1

n2c2t1t2c2c1

t2c2s4s0s6s8s5n1t2c2t1t2c2n1c2t1c2s7CTL的模型检验算法3,标记E[c2

Uc1]n1n2c2s3s2s1t1n2c2c1

n2c2t1t2c2c1

t2c2s4s0s6s8s5n1t2c2t1t2c2n1c2t1c2s7E[c2

Uc1]E[c2

Uc1]CTL的模型检验算法3,标记E[c2

Uc1]n1n2c2s3s2s1t1n2c2c1

n2c2t1t2c2c1

t2c2s4s0s6s8s5n1t2c2t1t2c2n1c2t1c2s7E[c2

Uc1]E[c2

Uc1]E[c2

Uc1]CTL的模型检验算法3,标记E[c2

Uc1]n1n2c2s3s2s1t1n2c2c1

n2c2t1t2c2c1

t2c2s4s0s6s8s5n1t2c2t1t2c2n1c2t1c2s7E[c2

Uc1]E[c2

Uc1]E[c2

Uc1]E[c2

Uc1]E[c2

Uc1]CTL的模型检验算法FunctionSAT()

begin case

isT: returnS

is: return

isatomic: return{s

S|L(s)}

is: returnS-SAT()

is12: returnSAT(1)SAT(2)

is12: returnSAT(1)SAT(2)

is12: returnSAT(12)

isAF: returnSATAF()

isEF: returnSAT

(E[ΤU])

isAX: returnSAT(EX)

isEX: returnSATEX()

isE[1U2]: returnSATEU(1,2)

isA[1U2]: returnSAT

((E[2U(12)]EG2))

isAG: returnSAT

(EF)

isEG: returnSAT(AF) endcaseendCTL的模型检验算法FunctionSATAF()

VarX,Ybegin

X:=S;

Y:=SAT(); repeatuntilX=Y begin

X:=Y;

Y:=Ypre(Y) end returnYendpre∀(Y)={s∈S|foralls’,(s→s’impliess’∈Y)}CTL的模型检验算法FunctionSATEX()

VarX,Ybegin

X:=SAT();

Y:=pre(X); returnYendpre(Y)={s∈S|exists’,(s→s’ands’∈Y)}CTL的模型检验算法FunctionSATEU(,)

VarX,Y,Wbegin

X:=S; W:=SAT(); Y:=SAT(); repeatuntilX=Y begin

X:=Y;

Y:=Y(Wpre(Y)) end returnYendCTL的模型检验算法标记算法的问题对模型的规模是线性的模型规模随变量个数成指数增长—状态爆炸克服状态爆炸方法有序二叉决策图符号模型检测有界模型检测LTL模型检验算法LTL的模型检测算法比CTL的复杂1、CTL公式是在状态上求值用状态能满足的子公式来标记系统的状态2、LTL子公式不是在状态上，而是沿着路径求值模型检测必须采取不同的策略LTL模型检验算法问题给定M，sS和，计算M,s|=

基本策略1、为构造接受的自动机A2、组合A和M，即求两者的公共路径集合3、搜索组合模型中是否存在从对应s的状态开始的路径存在：M,s|

不存在：M,s|=

LTL模型检验算法示例M如图：(aUb)路径：

s3,s4,s3,s2,s2,…迹(trace)：ab,ab,ab,ab,ab,…s2a

bs1abs4abs3abLTL模型检验算法1、构造接受(aUb)的自动机AaUbs2abs1abs4abs3abs3ab=aUbLTL模型检验算法2、合并A和M构造M的等价系统s2a

bs1abs4abs3abs2a

bs1abs4abs3abs3abLTL模型检验算法2、合并A和M合并（保留公共的迁移）s2a

bs1abs4abs3abs3abs2abs1abs4abs3abs3abLTL模型检验算法2、合并A和Ms2abs1abs4abs3abs3abLTL模型检验算法3、搜索组合模型中是否存在从对应s的状态开始的路径M,s|

反例s3,(s4,s3,)s2,s2,…s3,s4,(s3,s4,)s3,s1,s2,…s2abs1abs4abs3abs3ab构造自动机A求的子公式闭包：{a,b,a,b,aUb,(aUb)}对所有无前缀的，或(不同时)在s中s2