程序的形式验证 – 内容 中国科学院软件研究所 张文辉 http://lcs.ios.ac.cn/~zwh/pv

程序的形式验证 程序正确性: 测试 输入/输出 阅读 判断/分析/推理 形式验证 定义/性质/验证 int f(int n) { int x=n; int y=1; while (x!=0) { y=y*x; x--; } return y; } 2

程序形式验证的相关内容 程序正确性: 程序形式验证的基本概念 从系统运行角度考虑程序正确性问题 从程序设计的角度考虑程序正确性问题 系统运行模型的类型 系统性质的表示方法 验证方法 多种知识的应用(内容比较杂) 3

程序的形式验证 程序正确性: 程序正确性的最终体现: 以给定程序为主要组成部分的软件系统 具备我们期望的性质 4

程序正确性 程序 + 计算环境 性质 5

程序正确性 程序 + 计算环境 性质 系统模型 公式 6

形式验证 系统模型 公式 7

程序正确性的形式验证 软件 系统 运行过程 性质 抽象描述 或 模型 验证方法 逻辑公式 8

主要内容 程序正确性 系统运行模型 系统性质的表示 验证方法

程序正确性 从系统运行角度考虑问题: x=getnum(); y=1; while (x>1) { y=x*y; x=x-1; } printnum(y);

软件系统运行的正确性 程序 应用软件 软件系统运行 系统软件 计算机硬件 程序正确性 计算正确性 .

计算过程和结果 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’ ……

软件系统的每个运行的正确性 (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) -

每个运行的模型的正确性 (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) ------------------- (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) -------------------- . -

运行集合的模型的正确性 软件系统的运行模型的正确性 软件系统的模型的正确性 隐式迁移关系的描述 显式迁移关系的描述

隐式迁移关系的描述 x=n; y=1; while (x>1) { y=x*y; x=x-1; } z=y; 系统初始状态: x=0y=0 z=0m>n>0 (给定m) 系统终止要求: z=n! 系统运行要求: z!=0  z=n!

隐式迁移关系的描述 x=n; y=1; while (x>1) { y=x*y; x=x-1; z=y; } 系统初始状态: x=0y=0 z=0m>n>0 (给定m) 系统终止要求: z=n! 系统运行要求: z!=0  z=n!

显式迁移关系的描述 给定m=4 系统运行要求: (xi=1)  (yi+1=x1!) (s0,0,0) (s1,3,0) (s2,3,1)

程序的形式验证 程序正确性 软件系统运行/计算过程和结果的正确性 软件系统的每个运行的正确性 (测试) 软件系统的每个运行的模型的正确性 软件系统的运行集合的模型的正确性 软件系统的模型的正确性 (验证) 系统模型的有限表示 系统性质的逻辑表示 系统模型是否满足系统性质的验证方法

程序正确性 从程序设计的角度考虑问题: 系统需求 系统设计 代码生成/程序编写 编译

程序正确性 系统需求 系统设计 应用软件 软件系统运行 代码生成/程序编写 系统软件 编译 计算机硬件 系统设计是否满足系统需求?

程序正确性 系统需求 逻辑表示 (部分用) 系统设计 形式描述 (部分用) 代码生成/程序编写 程序 编译

系统需求 输入 正整数 输出 该整数的阶乘 以变量n代表输入值 以变量z代表输出值 系统初始状态的刻画(逻辑公式): n>0 系统终止状态的要求(逻辑公式): z=n!

系统设计(1) x=n; y=1; while (x>1) { y=x*y; x=x-1; } z=y; 系统初始状态: x=0y=0 z=0n>0 系统终止要求: z=n! 系统运行要求: z!=0  z=n!

系统设计(2) begin (x,y)=(n,1) s1 x>1 s2 s3 (x,y)=(x-1,y*x) (z)=(y) end

系统设计(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

系统设计(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

程序的形式验证 软件系统需求 软件系统设计 软件系统实现 (代码生成/程序编写) 软件系统的安装 软件系统的运行 部分系统需求的逻辑表示 部分系统设计的形式描述 系统设计是否满足系统需求的验证方法

系统运行模型 离散模型 混成模型 实时模型

离散系统运行模型(1) 系统运行(状态、迁移) 系统运行离散模型 r  (S) 或者说 r : N  S 或直接表示为r  (2AP) 系统运行集合 = { r | r  M } s0 s1 s2 s3

离散系统运行模型(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

离散系统运行模型(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

离散系统运行模型(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

混成系统运行模型 系统运行(离散部分、连续部分) 系统运行混成模型 设系统有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}

实时系统运行模型 系统运行(离散部分、时钟变量) 系统运行实时模型 设系统有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}

离散系统的表示 程序语言 状态迁移系统 -自动机 系统运行r  (S) 且 L: S  2AP {x=1,y=0} b c d s0 s1 s2 s3 系统运行r  (S) 且 L: S  2AP

运行集合的模型 (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) -------------------- . -

程序语言 s0: s1: s2: s3: s4: s5: s6: s7: x=n; y=1; while (x>1) { y=x*y; x=x-1; } z=y;

程序语言 系统运行 r  (S) 且 L: S  2AP 一般而言S和AP可以是无限集合 不存在一般的自动分析方法 {x=1,y=0}

状态迁移系统(状态、迁移) s000 s130 s231 s331 s431 s533 s120 s221 s321 s323 s412

状态迁移系统(状态、迁移、命题) s000 s130 s231 s331 s431 s533 {x=0,y=0} s120 s221

状态迁移系统 系统运行 r  (S) 且 L: S  2AP 要求S和AP是有穷集合 存在一般的自动分析方法 {x=1,y=0}

状态迁移系统/ -自动机 while (1) { x=getnum(); /* 4 > getnum() > 0 */ y=1; while (x>1) { y=x*y; x=x-1; } /* printnum(y); */

状态迁移系统/ -自动机 s000 s130 s231 s331 s431 s533 s120 s221 s321 s323 s412

状态迁移系统/ -自动机 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); */ }

-自动机(标号) 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

-自动机(标号、接受状态) 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

-自动机 s0 取钱 1 2 s1 s2 取茶 1 2 1 2 2 s6 s3 s4 s7 1 找钱/取钱 出茶 退钱 s5

-自动机 s0 取钱 1 2 s1 s2 取茶 1 2 1 2 2 s6 s3 s6 s4 s7 1 找钱/取钱 出茶 退钱 s5

-自动机 系统运行 r  (S) w  (Σ) 要求S和Σ是有穷集合 存在一般的自动分析方法 {x=1,y=0} a b c d s0 s1 s2 s3

混成系统的表示 混成自动机(离散、连续) 系统运行 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

混成自动机 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

混成自动机 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

混成自动机 水箱 x>=5 x:=x+1 on off x'=1 x<=9 x'=-1 x<=2

混成自动机 表达能力(有点太强)

混成自动机(阶乘算法) 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

混成自动机(阶乘算法) 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

混成自动机(阶乘算法) begin x:=n,y:=1 s1 x>1,x:=x-1,y:=y*x (x>1),z:=y end

混成自动机(阶乘算法) 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=1n=2n=3 z=n! end

混成自动机 系统运行 表示能力强 不存在一般的自动分析方法 0.1 0.2 0.1 s0 s1 s2 s3 {x=0.0,y=0.0} x'=20sqrt(x) (x=100t2) y'=1.0

实时系统的表示 时间自动机(离散、时间) 系统运行 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

时间自动机 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}

时间自动机 钥匙 open1 a,{x} a,x>1 a,x<=1 b b closed a b open5

时间自动机 s0 取钱 1 2 s1 s2 取茶 1 2 1 2 2 s6 s3 s6 s4 s7 1 找钱/取钱 出茶 退钱 s5

时间自动机 s0 取钱 1 2 s1 s2 取茶 1 2 1 2 2 s6 s3 s6 s4 s7 1 {x} 找钱/取钱 出茶 退钱 s5

时间自动机 系统运行 设系统有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}

系统性质的表示方法 死锁 终止 安全性质 活性 时序性质

线性时序性质 线性时序逻辑

线性时序性质 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>=0z=0  G(z!=0z=n!)

线性时序性质 0.1 1.2 时间线性时序逻辑 0.2 0.3 0.3

分枝时序性质 分枝时序逻辑

分枝时序逻辑 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>=0z=0  AG(z!=0z=n!)

分枝时序逻辑 n>=0  EF(z=1) n>=0z=0  EG(z!=0z=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>=0z=0  EG(z!=0z=1)

分枝时序性质 0.1 1.2 时间分枝时序逻辑 0.2 0.3

验证方法 推理验证方法(计算机辅助)： 自动验证方法： 基于推理规则 适用范围广 实用性受限于推理杂性和设计推理方案的难度 可能需要事先进行抽象处理以简化问题 证明失败不一定能说明什么问题 自动验证方法： 自动化 适用范围受限制 一般用于有限状态(数据简单控制复杂)的系统 最好事先进行抽象处理以简化问题 计算复杂性高、实用性受限于状态爆炸问题

课程主要内容 模型 语法、表示方法 语义、表示能力 逻辑 相关复杂性问题 验证 方法、算法、数据结构

预期目标 掌握并能够综合应用以下知识: 程序与 系统模型 验证方法 程序逻辑 基本原理 几类 简单的 几类 简单的 78

相关基础 逻辑、形式语言 集合、函数、图 算法、计算复杂性

参考文献

问题 ? 81