形式验证简介

1程序的形式验证-简介(2)中国科学院软件研究所张文辉~zwh/pv2程序验证给定一个程序和一些性质用严格的方法证明给定的程序是否满足给定的性质程序性质3程序验证给定一个程序和一些性质用严格的方法证明给定的程序是否满足给定的性质程序运行结果性质程序运行过程4程序验证给定一个程序和一些性质用严格的方法证明给定的程序是否满足给定的性质性质程序+运行环境软件系统运行过程5运行环境：例子默认环境数值计算：32位/64位人机交互：输入输出格式等远程控制：通讯设施网络环境：是否存在恶意攻击6程序验证性质软件系统运行过程逻辑公式抽象描述或模型验证方法7运行过程描述：例子s1:while(x==0)x=rand()%2;s2:while(true)skip;变量初始值：x=0或x=18s=1,x=0s=2,x=1s=1,x=1运行过程模型x=0x=1skipskip9运行过程描述s1:while(x==0)x=y;s2:while(true)skip;变量初始值：x=0或x=110y=0y=1运行环境y=1y=0y=1y=011运行环境描述t1:y=0;gotot2;t2:while(true)skip;变量初始值：y=1y=1y=0t=1,y=1t=2,y=012系统运行过程描述s1:while(x==0)x=y;s2:while(true)skip;变量初始值：x=0或x=1t1:y=0;gotot2;t2:while(true)skip;变量初始值：y=113s=1,x=0s=2,x=1s=1,x=1系统运行过程模型x=0x=1skipskipy=1y=014s=1,x=0,y=1s=2,x=1,y=1s=1,x=1,y=1系统运行过程模型x=1skipskips=1,x=0,y=0s=1,x=1,y=0s=2,x=1,y=015例子：互斥进程1:申请公共资源;获得并使用公共资源;释放公共资源;要求1：使用公共资源的进程数1进程2:申请公共资源;获得并使用公共资源;释放公共资源;要求2：若有进程申请则其后必有进程可以使用16程序验证的目的给定一个程序和一些性质用严格的方法证明给定的程序是否满足给定的性质程序性质抽象描述/模型逻辑公式验证方法17程序验证理论与方法•基础理论–形式语义–系统模型–时序逻辑•验证方法–对程序和系统描述进行推理分析–对系统模型进行基于图和算法的推理分析18逻辑推理：例子(1){x=0}while(x==0)x=y{x=1y=1}(2){y=1}y=y-1{y=0}(3){x=0}while(x==0)x=y;y=y-1;{y=0}19s=1,x=0,y=1s=2,x=1,y=1s=1,x=1,y=1图和算法的推理：例子x=1skipskips=1,x=0,y=0s=1,x=1,y=0s=2,x=1,y=0系统肯定能到达s=2或者x=0y=0的状态20相关内容•程序与系统模型–Kripke结构、符号迁移系统–ω-自动机、时间自动机、Petri网•程序性质与程序逻辑–命题逻辑、谓词逻辑–线性时序逻辑、分枝时序逻辑•分析验证方法–Hoare逻辑、可计算函数逻辑–基于状态的模型检测、基于路径的模型检测21•数理逻辑–描述系统、性质•自动机理论–描述系统、性质•形式语义–系统运行模型•图论、数据结构、算法设计与分析–搜索方法、算法、复杂性相关基础参考文献问题?23