程序的形式验证-简介

1、程序的形式验证 - 简介中国科学院软件研究所张文辉http:/ 测试 输入/输出 阅读 判断/分析/推理 形式验证 定义/性质/验证程序正确性: int f(int n) int x=n; int y=1; while (x!=0) y=y*x; x-; return y; 3形式验证简介的内容 程序形式验证的基本概念 从系统运行角度考虑程序正确性问题 从程序设计的角度考虑程序正确性问题 系统运行模型的类型 系统性质的表示方法 验证方法程序正确性:多种知识的应用(内容比较杂)4程序的形式验证 程序正确性的最终体现:以给定程序为主要组成部分的软件系统具备我们期望的性质程序正确性:5程序正确性程序

2、+计算环境性质6程序正确性程序+计算环境性质系统模型公式7形式验证系统模型公式8程序正确性的形式验证性质软件系统运行过程逻辑公式抽象描述或模型验证方法程序正确性从系统运行角度考虑问题: x=getnum(); y=1; while (x1) y=x*y;x=x-1; printnum(y);软件系统运行的正确性计算机硬件系统软件应用软件程序软件系统运行程序正确性 计算正确性 .计算过程和结果运行时刻 0: (l,x,y)=(,0,0)运行时刻 1: (l,x,y)=(,5,0)运行时刻 2: (l,x,y)=(,5,1)运行时刻 3: (l,x,y)=(,.,.)运行时刻 4:0 1 2 3

3、4 0 1 2 3 4 x=getnum(); y=1; while (x1) y=x*y;x=x-1; printnum(y);软件系统的每个运行的正确性(pc,x,y)=(.,0,0)-(pc,x,y)=(.,3,0)(pc,x,y)=(.,3,1)(pc,x,y)=(.,3,1)(pc,x,y)=(.,3,3)(pc,x,y)=(.,2,3)(pc,x,y)=(.,2,3)(pc,x,y)=(.,2,6)(pc,x,y)=(.,1,6)(pc,x,y)=(.,1,6)-(pc,x,y)=(.,1,6)(pc,x,y)=(.,0,0)-(pc,x,y)=(.,2,0)(pc,x,y)=(.

4、,2,1)(pc,x,y)=(.,2,1)(pc,x,y)=(.,2,2)(pc,x,y)=(.,1,2)(pc,x,y)=(.,1,2)-(pc,x,y)=(.,1,2)-每个运行的模型的正确性(pc,x,y)=(s0,0,0)-(pc,x,y)=(s1,3,0)(pc,x,y)=(s2,3,1)(pc,x,y)=(s3,3,1)(pc,x,y)=(s4,3,3)(pc,x,y)=(s5,2,3)(pc,x,y)=(s3,2,3)(pc,x,y)=(s4,2,6)(pc,x,y)=(s5,1,6)(pc,x,y)=(s6,1,6)-(pc,x,y)=(s7,1,6)(pc,x,y)=(s0,

5、0,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)=(s2,3,1)(pc,x,y)=(s3,3,1)(pc,x,y)=(s4,3,3)(pc,x,y)=(s5,2,3)(pc,x,y)=(s3,2,3)(pc,x,y)=(s4,2,6)(pc,x,y)=(s5,1,6)(pc,x,y)=

6、(s6,1,6)-(pc,x,y)=(s7,1,6)(pc,x,y)=(s0,0,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 (x1) y=x*y;x=x-1; z=y; 系统初始状态: x=0y=

7、0 z=0mn0 (给定m) 系统终止要求: z=n! 系统运行要求: z!=0 z=n!隐式迁移关系的描述 x=n; y=1; while (x1) y=x*y;x=x-1; z=y; 系统初始状态: x=0y=0 z=0mn0 (给定m) 系统终止要求: z=n! 系统运行要求: z!=0 z=n!显式迁移关系的描述(s0,0,0)(s1,3,0)(s2,3,1)(s3,3,1)(s4,3,3)(s5,2,3)(s3,2,3)(s4,2,6)(s5,1,6)(s6,1,6)(s1,2,0)(s2,2,1)(s3,2,1)(s4,2,2)(s5,1,2)(s6,1,2)给定m=4系统运行要求

8、: (xi=1) (yi+1=x1!)(s1,1,0)(s2,1,1)(s6,1,1)程序的形式验证 程序正确性 软件系统运行/计算过程和结果的正确性 软件系统的每个运行的正确性 (测试) 软件系统的每个运行的模型的正确性 软件系统的运行集合的模型的正确性 软件系统的模型的正确性 (验证) 系统模型的有限表示 系统性质的逻辑表示 系统模型是否满足系统性质的验证方法程序正确性从程序设计的角度考虑问题:系统需求系统设计代码生成/程序编写编译程序正确性系统需求系统设计代码生成/程序编写编译计算机硬件系统软件应用软件软件系统运行系统设计是否满足系统需求?程序正确性系统需求系统设计代码生成/程序编写编译

9、程序逻辑表示形式描述(部分用)(部分用)系统需求 输入 正整数 输出 该整数的阶乘 以变量n代表输入值 以变量z代表输出值 系统初始状态的刻画(逻辑公式): n0 系统终止状态的要求(逻辑公式): z=n!系统设计(1) x=n; y=1; while (x1) y=x*y;x=x-1; z=y; 系统初始状态: x=0y=0 z=0n0 系统终止要求: z=n! 系统运行要求: z!=0 z=n!系统设计(2)begin(x,y)=(n,1)s1s3end(z)=(y)x1s2(x,y)=(x-1,y*x)系统设计(2)begin(x,y)=(n,1)s1s3end(z)=(y)x1s2(x

10、,y)=(x-1,y*x)4n0z=n!系统设计(2)begin(x,y)=(n,1)s1s3end(z)=(y)x1s2(x,y)=(x-1,y*x)4n0,z=0z=n!z!=0 z=n!程序的形式验证 软件系统需求 软件系统设计 软件系统实现 (代码生成/程序编写) 软件系统的安装 软件系统的运行 部分系统需求的逻辑表示 部分系统设计的形式描述 系统设计是否满足系统需求的验证方法程序正确性系统运行模型的一些类型 离散模型 混成模型 实时模型离散系统运行模型(1) 系统运行(状态、迁移) 系统运行离散模型 r (S) 或者说 r : N S 或直接表示为r (2AP) 系统运行集合 = r

11、 | r M s0s1s2s3离散系统运行模型(2) 系统运行(状态、迁移、状态基本信息) 系统运行离散模型 r (S) 且 L: S 2AP 或者说 r : N S 或直接表示为r (2AP) 或 r : N 2AP 系统运行集合 = r | r M s0s1s2s3x=1,y=0 x=1,y=1离散系统运行模型(3) 系统运行(动作信息) 系统运行离散模型 r (S) 且 w () 系统运行集合 = r | r M(S) 系统标号集合 = w | w M() s0s1s2s3x=1,y=0 x=1,y=1cbda离散系统运行模型(4) 系统运行(动作信息、接受条件) 系统运行离散模型 r

12、(S) 且 w () 系统运行集合 = r | r M(S) (符合接受条件) 系统标号集合 = w | w M() s0s1s2s3x=1,y=0 x=1,y=1cbda混成系统运行模型 系统运行(离散部分、连续部分) 系统运行混成模型 设系统有k个实数变量 r : S k 系统运行集合 = r | r M x=0.0,y=0.0 x=1.0,y=0.1x=4.0,y=0.3s0s1s2scbda实时系统运行模型 系统运行(离散部分、时钟变量) 系统运行实时模型 设系统有k个时钟变量 r : S k 运行的刻画可以简化为 r : N S kx=0.0,y=0.0 x=0.

13、0,y=0.1x=0.0,y=0.3s0s1s2scbda离散系统的表示 程序语言 状态迁移系统 -自动机s0s1s2s3x=1,y=0 x=1,y=1cbda系统运行r (S) 且 L: S 2AP运行集合的模型(pc,x,y)=(s0,0,0)-(pc,x,y)=(s1,3,0)(pc,x,y)=(s2,3,1)(pc,x,y)=(s3,3,1)(pc,x,y)=(s4,3,3)(pc,x,y)=(s5,2,3)(pc,x,y)=(s3,2,3)(pc,x,y)=(s4,2,6)(pc,x,y)=(s5,1,6)(pc,x,y)=(s6,1,6)-(pc,x,y)=(s

14、7,1,6)(pc,x,y)=(s0,0,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 (x1) y=x*y;x=x-1; z=y; 程序语言 系统运行 r (S) 且 L: S 2AP 一般而言S和AP可以是无限集合 不存在一般的自动分析方法s0s1s2s3x=1,

15、y=0 x=1,y=1状态迁移系统(状态、迁移)s000s130s231s331s431s533s323s425s516s616s120s221s321s412s512s612s110s211s611状态迁移系统(状态、迁移、命题)s000s130s231s331s431s533s323s425s516s616s120s221s321s412s512s612s110s211s611x=0,y=0 x=1,y=0 x=1,y=1状态迁移系统 系统运行 r (S) 且 L: S 2AP 要求S和AP是有穷集合 存在一般的自动分析方法s0s1s2s3x=1,y=0 x=1,y=1状态迁移系统/ -自

16、动机while (1) x=getnum(); /* 4 getnum() 0 */ y=1; while (x1) y=x*y; x=x-1; /* printnum(y); */ 状态迁移系统/ -自动机s000s130s231s331s431s533s323s425s516s616s120s221s321s412s512s612s110s211s611状态迁移系统/ -自动机while (1) (a) x=getnum(); /* 4 getnum() 0 */ (b) y=1; (c) while (x1) (b) y=x*y; (d) x=x-1; (e) /* printnum(y

17、); */ -自动机(标号)s000s130s231s331s433s523s323s426s516s120s221s321s412s512s612abbbaccbbdcddceecas110s211s611bces616Labels: a,b,c,d,e-自动机(标号、接受状态)s000s130s231s331s433s523s323s426s516s120s221s321s412s512s612abbbaccbbdcddceecas110s211s611bces616Labels: a,b,c,d,e-自动机s011121取茶s1s3s52s22s4找钱/取钱2退钱s6s7出茶取钱-自动机

18、s011121取茶s1s3s52s22s4找钱/取钱2退钱s6s7出茶取钱s6-自动机 系统运行 r (S) w () 要求S和是有穷集合 存在一般的自动分析方法s0s1s2s3x=1,y=0 x=1,y=1cbda混成系统的表示 混成自动机(离散、连续)x=0.0,y=0.0 x=1.0,y=0.1x=4.0,y=0.3s0s1s2scbda系统运行 r : S k混成自动机s000s130s231s331s433s523s323s426s516s120s221s321s412s512s612b,x=0.2,x:=0bac,x=0.1,x:=0cbdces110s211s

19、611bces616a,x5,x:=0,y:=0b,x=0.4,x:=0d,x=0.2,x:=0c,x=0.1,x:=0b,x=0.6,x:=0d,x=0.2,x:=0c,x=0.1,x:=0e,x=0.1,x:=0,z:=0Variables: x(时间),y(累计),z(费用)混成自动机s000s130s231s331s433s523s323s426s516s120s221s321s412s512s612b,x=0.2,x:=0bac,x=0.1,x:=0cbdces110s211s611bces616a,x5,x:=0,y:=0b,x=0.4,x:=0d,x=0.2,x:=0c,x=0.

20、1,x:=0b,x=0.6,x:=0d,x=0.2,x:=0c,x=0.1,x:=0e,x=0.1,x:=0,z:=0Variables: x(时间),y(累计),z(费用)x=1y=1z=1x=1y=1z=2混成自动机 水箱x=5x:=x+1x=1x1s2(x,y)=(x-1,y*x)4n0,z=0z=n!z!=0 z=n!混成自动机(阶乘算法)begin(x,y)=(n,1)s1end(z)=(y)x1(x,y)=(x-1,y*x)(x1)4n0,z=0z=n!z!=0 z=n!混成自动机(阶乘算法)begins1end(x1),z:=yx1,x:=x-1,y:=y*xx:=n,y:=1混

21、成自动机(阶乘算法)begins1end(x1),z:=yx1,x:=x-1,y:=y*xx:=n,y:=1x=0y=0z=0n=0 x=0y=0z=0n=0 x=0y=0z=0n=0变量初始值：x=0y=0z=0n=1n=2n=3z=n!混成自动机 系统运行 表示能力强 不存在一般的自动分析方法x=0.0,y=0.0 x=1.0,y=0.1 x=4.0,y=0.3x=10y=1.0 x=15y=1.0 x=20sqrt(x) (x=100t2)y=1.0s0s1s2s实时系统的表示 时间自动机(离散、时间)x=0.0,y=0.0 x=0.0,y=0.1x=0.0,y=0.

22、3s0s1s2scbda系统运行 r : N S k时间自动机s000s130s231s331s433s523s323s426s516s120s221s321s412s512s612b,x=0.2,xbac,x=0.1,xcbdces110s211s611bces616a,x5,x,yb,x=0.4,xd,x=0.2,xc,x=0.1,xb,x=0.6,xd,x=0.2,xc,x=0.1,xe,x=0.1,x,zClocks: x,y,z时间自动机 钥匙ba,xclosedopen5open1a,x1bab时间自动机s011121取茶s1s3s52s22s4找钱/取钱2退钱s6s7出茶取钱s6时间自动机s011121取茶s1s3s52s22s4找钱/取钱2退钱s6s7出茶取钱s6xx=10时间自动机 系统运行 设系统有k个时钟变量 r : N S k 存在一般的自动分析方法x=0.0,y=0.0 x=0.0,y=0.1s0s1s2sx=0.0,y=0.3程序正确性系统性质的表示方法: 死锁 终止 安全性质 活性 时序性质线性时序性质 线