Download presentation
Presentation is loading. Please wait.
1
程序的形式验证 – 内容 中国科学院软件研究所 张文辉
2
程序的形式验证 程序正确性: 测试 输入/输出 阅读 判断/分析/推理 形式验证 定义/性质/验证 int f(int n) {
int x=n; int y=1; while (x!=0) { y=y*x; x--; } return y; } 2
3
程序形式验证的相关内容 程序正确性: 程序形式验证的基本概念 从系统运行角度考虑程序正确性问题 从程序设计的角度考虑程序正确性问题
系统运行模型的类型 系统性质的表示方法 验证方法 多种知识的应用(内容比较杂) 3
4
程序的形式验证 程序正确性: 程序正确性的最终体现: 以给定程序为主要组成部分的软件系统 具备我们期望的性质 4
5
程序正确性 程序 + 计算环境 性质 5
6
程序正确性 程序 + 计算环境 性质 系统模型 公式 6
7
形式验证 系统模型 公式 7
8
程序正确性的形式验证 软件 系统 运行过程 性质 抽象描述 或 模型 验证方法 逻辑公式 8
9
主要内容 程序正确性 系统运行模型 系统性质的表示 验证方法
10
程序正确性 从系统运行角度考虑问题: x=getnum(); y=1; while (x>1) { y=x*y; x=x-1; }
printnum(y);
11
软件系统运行的正确性 程序 应用软件 软件系统运行 系统软件 计算机硬件 程序正确性 计算正确性
12
计算过程和结果 x=getnum(); y=1; while (x>1) { y=x*y; x=x-1; } printnum(y);
运行时刻 0: (pc,x,y)=(…,0,0) 运行时刻 1: (pc,x,y)=(…,5,0) 运行时刻 2: (pc,x,y)=(…,5,1) 运行时刻 3: (pc,x,y)=(…,..,..) 运行时刻 4: 0 1 2 3 4 …… 0 ’1’ 2’ 3 ’4’ ……
13
软件系统的每个运行的正确性 (pc,x,y)=(..,0,0) ------------------- (pc,x,y)=(..,3,0)
(pc,x,y)=(..,2,0) (pc,x,y)=(..,2,1) (pc,x,y)=(..,2,2) (pc,x,y)=(..,1,2) -
14
每个运行的模型的正确性 (pc,x,y)=(s0,0,0) ------------------- (pc,x,y)=(s1,3,0)
(pc,x,y)=(s1,2,0) (pc,x,y)=(s2,2,1) (pc,x,y)=(s3,2,1) (pc,x,y)=(s4,2,2) (pc,x,y)=(s5,1,2) (pc,x,y)=(s6,1,2) (pc,x,y)=(s7,1,2) -
15
运行集合的模型的正确性 (pc,x,y)=(s0,0,0) ------------------- (pc,x,y)=(s1,3,0)
(pc,x,y)=(s1,2,0) (pc,x,y)=(s2,2,1) (pc,x,y)=(s3,2,1) (pc,x,y)=(s4,2,2) (pc,x,y)=(s5,1,2) (pc,x,y)=(s6,1,2) (pc,x,y)=(s7,1,2) - (pc,x,y)=(s0,0,0) . -
16
运行集合的模型的正确性 软件系统的运行模型的正确性 软件系统的模型的正确性 隐式迁移关系的描述 显式迁移关系的描述
17
隐式迁移关系的描述 x=n; y=1; while (x>1) { y=x*y; x=x-1; } z=y; 系统初始状态: x=0y=0 z=0m>n>0 (给定m) 系统终止要求: z=n! 系统运行要求: z!=0 z=n!
18
隐式迁移关系的描述 x=n; y=1; while (x>1) { y=x*y; x=x-1; z=y; } 系统初始状态: x=0y=0 z=0m>n>0 (给定m) 系统终止要求: z=n! 系统运行要求: z!=0 z=n!
19
显式迁移关系的描述 给定m=4 系统运行要求: (xi=1) (yi+1=x1!) (s0,0,0) (s1,3,0) (s2,3,1)
20
程序的形式验证 程序正确性 软件系统运行/计算过程和结果的正确性 软件系统的每个运行的正确性 (测试) 软件系统的每个运行的模型的正确性
软件系统的运行集合的模型的正确性 软件系统的模型的正确性 (验证) 系统模型的有限表示 系统性质的逻辑表示 系统模型是否满足系统性质的验证方法
21
程序正确性 从程序设计的角度考虑问题: 系统需求 系统设计 代码生成/程序编写 编译
22
程序正确性 系统需求 系统设计 应用软件 软件系统运行 代码生成/程序编写 系统软件 编译 计算机硬件 系统设计是否满足系统需求?
23
程序正确性 系统需求 逻辑表示 (部分用) 系统设计 形式描述 (部分用) 代码生成/程序编写 程序 编译
24
系统需求 输入 正整数 输出 该整数的阶乘 以变量n代表输入值 以变量z代表输出值 系统初始状态的刻画(逻辑公式): n>0 系统终止状态的要求(逻辑公式): z=n!
25
系统设计(1) x=n; y=1; while (x>1) { y=x*y; x=x-1; } z=y; 系统初始状态: x=0y=0 z=0n>0 系统终止要求: z=n! 系统运行要求: z!=0 z=n!
26
系统设计(2) begin (x,y)=(n,1) s1 x>1 s2 s3 (x,y)=(x-1,y*x) (z)=(y) end
27
系统设计(2) begin (x,y)=(n,1) 4>n>0 s1 x>1 z=n! s2 s3
(x,y)=(x-1,y*x) (z)=(y) end
28
系统设计(2) z!=0 z=n! begin (x,y)=(n,1) 4>n>0,z=0 s1 x>1 z=n!
(x,y)=(x-1,y*x) (z)=(y) end
29
程序的形式验证 软件系统需求 软件系统设计 软件系统实现 (代码生成/程序编写) 软件系统的安装 软件系统的运行 部分系统需求的逻辑表示
部分系统设计的形式描述 系统设计是否满足系统需求的验证方法
30
系统运行模型 离散模型 混成模型 实时模型
31
离散系统运行模型(1) 系统运行(状态、迁移) 系统运行离散模型 r (S) 或者说 r : N S
或直接表示为r (2AP) 系统运行集合 = { r | r M } s0 s1 s2 s3
32
离散系统运行模型(2) 系统运行(状态、迁移、状态基本信息) 系统运行离散模型 r (S) 且 L: S 2AP
或者说 r : N S 或直接表示为r (2AP) 或 r : N 2AP 系统运行集合 = { r | r M } {x=1,y=0} {x=1,y=1} s0 s1 s2 s3
33
离散系统运行模型(3) 系统运行(动作信息) 系统运行离散模型 r (S) 且 w (Σ)
系统运行集合 = { r | r M(S) } 系统标号集合 = { w | w M(Σ) } {x=1,y=0} {x=1,y=1} a b c d s0 s1 s2 s3
34
离散系统运行模型(4) 系统运行(动作信息、接受条件) 系统运行离散模型 r (S) 且 w (Σ)
系统运行集合 = { r | r M(S) (符合接受条件) } 系统标号集合 = { w | w M(Σ) } {x=1,y=0} {x=1,y=1} a b c d s0 s1 s2 s3
35
混成系统运行模型 系统运行(离散部分、连续部分) 系统运行混成模型 设系统有k个实数变量 r : Ｒ S Ｒk
系统运行集合 = { r | r M } 0.1 0.2 0.1 a b c d s0 s1 s2 s3 {x=0.0,y=0.0} {x=1.0,y=0.1} {x=4.0,y=0.3}
36
实时系统运行模型 系统运行(离散部分、时钟变量) 系统运行实时模型 设系统有k个时钟变量 r : Ｒ S Ｒk
运行的刻画可以简化为 r : N S ＲＲk 0.1 0.2 0.1 a b c d s0 s1 s2 s3 {x=0.0,y=0.0} {x=0.0,y=0.1} {x=0.0,y=0.3}
37
离散系统的表示 程序语言 状态迁移系统 -自动机 系统运行r (S) 且 L: S 2AP {x=1,y=0}
b c d s0 s1 s2 s3 系统运行r (S) 且 L: S 2AP
38
运行集合的模型 (pc,x,y)=(s0,0,0) ------------------- (pc,x,y)=(s1,3,0)
(pc,x,y)=(s1,2,0) (pc,x,y)=(s2,2,1) (pc,x,y)=(s3,2,1) (pc,x,y)=(s4,2,2) (pc,x,y)=(s5,1,2) (pc,x,y)=(s6,1,2) (pc,x,y)=(s7,1,2) - (pc,x,y)=(s0,0,0) . -
39
程序语言 s0: s1: s2: s3: s4: s5: s6: s7: x=n; y=1; while (x>1) { y=x*y;
x=x-1; } z=y;
40
程序语言 系统运行 r (S) 且 L: S 2AP 一般而言S和AP可以是无限集合 不存在一般的自动分析方法 {x=1,y=0}
41
状态迁移系统(状态、迁移) s000 s130 s231 s331 s431 s533 s120 s221 s321 s323 s412
42
状态迁移系统(状态、迁移、命题) s000 s130 s231 s331 s431 s533 {x=0,y=0} s120 s221
43
状态迁移系统 系统运行 r (S) 且 L: S 2AP 要求S和AP是有穷集合 存在一般的自动分析方法 {x=1,y=0}
44
状态迁移系统/ -自动机 while (1) { x=getnum(); /* 4 > getnum() > 0 */ y=1; while (x>1) { y=x*y; x=x-1; } /* printnum(y); */
45
状态迁移系统/ -自动机 s000 s130 s231 s331 s431 s533 s120 s221 s321 s323 s412
46
状态迁移系统/ -自动机 while (1) { (a) x=getnum(); /* 4 > getnum() > 0 */ (b) y=1; (c) while (x>1) { (b) y=x*y; (d) x=x-1; } (e) /* printnum(y); */ }
47
-自动机(标号) a b c b d s000 s130 s231 s331 s433 s523 c a c b b s120 s221
e e s611 s612 s616 e Labels: a,b,c,d,e
48
-自动机(标号、接受状态) a b c b d s000 s130 s231 s331 s433 s523 c a c b b s120
e e s611 s612 s616 e Labels: a,b,c,d,e
49
-自动机 s0 取钱 1 2 s1 s2 取茶 1 2 1 2 2 s6 s3 s4 s7 1 找钱/取钱 出茶 退钱 s5
50
-自动机 s0 取钱 1 2 s1 s2 取茶 1 2 1 2 2 s6 s3 s6 s4 s7 1 找钱/取钱 出茶 退钱 s5
51
-自动机 系统运行 r (S) w (Σ) 要求S和Σ是有穷集合 存在一般的自动分析方法 {x=1,y=0}
a b c d s0 s1 s2 s3
52
混成系统的表示 混成自动机(离散、连续) 系统运行 r : Ｒ S Ｒk 0.1 0.2 0.1 a b c d s0 s1 s2
{x=0.0,y=0.0} {x=1.0,y=0.1} {x=4.0,y=0.3} 系统运行 r : Ｒ S Ｒk
53
混成自动机 a,x<5,x:=0,y:=0 c,x=0.1,x:=0 d,x=0.2,x:=0 s000 s130 s231 s331
b,x=0.2,x:=0 b,x=0.4,x:=0 s523 a c,x=0.1,x:=0 c b b s120 s221 s321 s323 b,x=0.6,x:=0 s412 d b s426 d,x=0.2,x:=0 s110 s211 s512 c c s516 e c,x=0.1,x:=0 e s611 s612 s616 Variables: x(时间),y(累计),z(费用) e,x=0.1,x:=0,z:=0
54
混成自动机 a,x<5,x:=0,y:=0 c,x=0.1,x:=0 d,x=0.2,x:=0 s000 s130 s231 s331
b,x=0.2,x:=0 b,x=0.4,x:=0 s523 a c,x=0.1,x:=0 c b b x’=1 y’=1 z’=1 s120 s221 s321 s323 b,x=0.6,x:=0 s412 d b s426 d,x=0.2,x:=0 x’=1 y’=1 z’=2 s110 s211 s512 c c s516 e c,x=0.1,x:=0 e s611 s612 s616 Variables: x(时间),y(累计),z(费用) e,x=0.1,x:=0,z:=0
55
混成自动机 水箱 x>=5 x:=x+1 on off x'=1 x<=9 x'=-1 x<=2
56
混成自动机 表达能力(有点太强)
57
混成自动机(阶乘算法) z!=0 z=n! begin (x,y)=(n,1) 4>n>0,z=0 s1 x>1
(x,y)=(x-1,y*x) (z)=(y) end
58
混成自动机(阶乘算法) z!=0 z=n! begin (x,y)=(n,1) 4>n>0,z=0 s1 x>1
(x,y)=(x-1,y*x) (z)=(y) z=n! end
59
混成自动机(阶乘算法) begin x:=n,y:=1 s1 x>1,x:=x-1,y:=y*x (x>1),z:=y end
60
混成自动机(阶乘算法) x'=0 y'=0 z'=0 n'=0 begin x:=n,y:=1 x'=0 y'=0 z'=0 n'=0 s1
x>1,x:=x-1,y:=y*x (x>1),z:=y x'=0 y'=0 z'=0 n'=0 变量初始值： x=0 y=0 z=0 n=1n=2n=3 z=n! end
61
混成自动机 系统运行 表示能力强 不存在一般的自动分析方法 0.1 0.2 0.1 s0 s1 s2 s3 {x=0.0,y=0.0}
x'=20sqrt(x) (x=100t2) y'=1.0
62
实时系统的表示 时间自动机(离散、时间) 系统运行 r : N S ＲＲk 0.1 0.2 0.1 a b c d s0 s1 s2
{x=0.0,y=0.0} {x=0.0,y=0.1} {x=0.0,y=0.3} 系统运行 r : N S ＲＲk
63
时间自动机 a,x<5,{x,y} c,x=0.1,{x} d,x=0.2,{x} s000 s130 s231 s331 s433
b,x=0.2,{x} b,x=0.4,{x} s523 a c,x=0.1,{x} c b b s120 s221 s321 s323 b,x=0.6,{x} s412 d b s426 d,x=0.2,{x} s110 s211 s512 c c s516 e c,x=0.1,{x} e s611 s612 s616 Clocks: x,y,z e,x=0.1,{x,z}
64
时间自动机 钥匙 open1 a,{x} a,x>1 a,x<=1 b b closed a b open5
65
时间自动机 s0 取钱 1 2 s1 s2 取茶 1 2 1 2 2 s6 s3 s6 s4 s7 1 找钱/取钱 出茶 退钱 s5
66
时间自动机 s0 取钱 1 2 s1 s2 取茶 1 2 1 2 2 s6 s3 s6 s4 s7 1 {x} 找钱/取钱 出茶 退钱 s5
67
时间自动机 系统运行 设系统有k个时钟变量 r : N S ＲＲk 存在一般的自动分析方法 0.1 0.2 0.1 s0 s1 s2
{x=0.0,y=0.0} {x=0.0,y=0.1} {x=0.0,y=0.3}
68
系统性质的表示方法 死锁 终止 安全性质 活性 时序性质
69
线性时序性质 线性时序逻辑
70
线性时序性质 F(z=n!) n>=0 F(z=n!) G(z!=0 z=n!)
begin (x,y)=(n,1) z!=0 z=n! n>=0,z=0 s1 x>1 z=n! s2 s3 (x,y)=(x-1,y*x) (z)=(y) end F(z=n!) n>=0 F(z=n!) G(z!=0 z=n!) n>=0z=0 G(z!=0z=n!)
71
线性时序性质 0.1 1.2 时间线性时序逻辑 0.2 0.3 0.3
72
分枝时序性质 分枝时序逻辑
73
分枝时序逻辑 AF(z=n!) n>=0 F(z=n!) AG(z!=0 z=n!)
begin (x,y)=(n,1) z!=0 z=n! n>=0,z=0 s1 x>1 z=n! s2 s3 (x,y)=(x-1,y*x) (z)=(y) end AF(z=n!) n>=0 F(z=n!) AG(z!=0 z=n!) n>=0z=0 AG(z!=0z=n!)
74
分枝时序逻辑 n>=0 EF(z=1) n>=0z=0 EG(z!=0z=1) z!=0 z=n! begin
(x,y)=(n,1) z!=0 z=n! n>=0,z=0 s1 x>1 z=n! s2 s3 (x,y)=(x-1,y*x) (z)=(y) end n>=0 EF(z=1) n>=0z=0 EG(z!=0z=1)
75
分枝时序性质 0.1 1.2 时间分枝时序逻辑 0.2 0.3
76
验证方法 推理验证方法(计算机辅助)： 自动验证方法： 基于推理规则 适用范围广 实用性受限于推理杂性和设计推理方案的难度
可能需要事先进行抽象处理以简化问题 证明失败不一定能说明什么问题 自动验证方法： 自动化 适用范围受限制 一般用于有限状态(数据简单控制复杂)的系统 最好事先进行抽象处理以简化问题 计算复杂性高、实用性受限于状态爆炸问题
77
课程主要内容 模型 语法、表示方法 语义、表示能力 逻辑 相关复杂性问题 验证 方法、算法、数据结构
78
预期目标 掌握并能够综合应用以下知识: 程序与 系统模型 验证方法 程序逻辑 基本原理 几类 简单的 几类 简单的 78
79
相关基础 逻辑、形式语言 集合、函数、图 算法、计算复杂性
80
参考文献
81
问题 ? 81
Similar presentations
