Download presentation
Presentation is loading. Please wait.
1
中国科学院软件研究所 计算机科学国家重点实验室 张文辉 http://lcs.ios.ac.cn/~zwh/
中国科学院研究生院信息科学与工程学院课程 程序的形式验证 – 简介 中国科学院软件研究所 计算机科学国家重点实验室 张文辉
2
程序正确性的重要性 应用广泛 软件错误的可能后果 航空 航天 金融 设备的控制 日常生活
火箭 Ariane 5 Explosion (1997) 火星气候轨道器 NASA Mars Climate Orbiter (1999)
3
程序正确性方法 测试 形式验证 黑盒测试 白盒测试 推理验证 模型检测 可执行代码 程序代码 程序代码或其抽象模型 程序运行环境模型 规则
算法
4
例子: ISR ./isr INFO: system is now active N: 2 RESULT: 1 N: 10
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { ./isr INFO: system is now active N: RESULT: 1 N: RESULT: 3 N: RESULT: 4 N: INFO: the input number must be in {0,...,20} N: RESULT: 2 N:
5
例子: ISR 输入为0和20之间的整数时， 输出为其平方根的整数部分。 对ISR的要求: 输入为0和20之间的整数时，
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { 对ISR的要求: 输入为0和20之间的整数时， 输出为其平方根的整数部分。 输入为0和20之间的整数时， 输出为其平方根的整数部分。
6
测试 黑盒测试 白盒测试 Program testing can be used to show the presence of bugs, but never to show their absence! -- Edsger W. Dijkstra
7
形式验证 推理验证 模型检测 正确性 正确性+不正确性
8
例子: ISR 对ISR的要求: (at line 18):((m*m)<=n)&&((m*m)+2*m+1>n)
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { 对ISR的要求: (at line 18):((m*m)<=n)&&((m*m)+2*m+1>n)
9
模型检测 ./verds –c isr.c –sp isr.sp 验证结果 反例
10
验证过程 Automatic Translator C Program Model VERDS Model Checker
Specification Negative Conclusion Error Trace
11
反例分析 以下输入产生不正确结果 不正确运行
12
修正后的例子: ISR2 ./isr2 INFO: system is now active N: 2 RESULT: 1 N: 10
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { ./isr2 INFO: system is now active N: RESULT: 1 N: RESULT: 3 N: RESULT: 4 N: INFO: the input number must be in {0,...,20} N: RESULT: 2 N:
13
模型检测 ./verds –c isr2.c –sp isr.sp 验证结果
14
验证过程 Automatic Translator C Program Model VERDS Model Checker
Specification Positive Conclusion
15
模型检测的缺点与优点 缺点 可直接验证的程序规模小 可直接验证的程序结构简单 优点: 自动验证 对不正确的程序可生成诊断信息
16
推理验证 main(int argc, char **argv ) { int n=0; int m=0; int k=1;
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { main(int argc, char **argv ) { int n=0; int m=0; int k=1; printf("system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); }
17
推理验证 main(int argc, char **argv ) { int n=0; int m=0; int k=1;
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { main(int argc, char **argv ) { int n=0; int m=0; int k=1; printf("system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } n>=0; n<=20; k!=20; k>=0; ((m*m)<=n)&&((m*m)+2*m+1>n);
18
推理验证(1) int in() { char c=0; int k=0; while (1) { k=0; …
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { int in() { char c=0; int k=0; while (1) { k=0; … if (c=='\n') { return k; } return k; } k>=0; k<=20; 不可达 k>=0; k<=20;
19
推理验证(2) int isk(int n,int k) { if (k!=20) { if (k!=n) k=21;
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { int isk(int n,int k) { if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; } return k; k>=0; k!=20; k>=0;
20
推理验证(3) int isr(int x,int k) { int y1=0; int y2=0; int y3=0;
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { int isr(int x,int k) { int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; } return y1; x>=0; k>=0; (x>2&&k==20): ((y1*y1)<=x-1)&&((y1*y1)+2*y1+1>x-1); !(x>2&&k==20): ((y1*y1)<=x)&&((y1*y1)+2*y1+1>x);
21
推理验证 main(int argc, char **argv ) { int n=0; int m=0; int k=1;
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { main(int argc, char **argv ) { int n=0; int m=0; int k=1; printf("system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } n>=0; n<=20; k!=20; k>=0; (n>2&&k==20): ((m*m)<=n-1)&&((m*m)+2*m+1>n-1); !(n>2&&k==20): ((m*m)<=n)&&((m*m)+2*m+1>n);
22
推理验证 main(int argc, char **argv ) { int n=0; int m=0; int k=1;
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { main(int argc, char **argv ) { int n=0; int m=0; int k=1; printf("system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } n>=0; n<=20; k!=20; k>=0; ((m*m)<=n)&&((m*m)+2*m+1>n);
23
推理验证的缺点与优点 缺点 原则上不能自动化 验证人员需要知道程序关键部位的关键性质 对确认程序的不正确难度大 优点 可验证任意规模的模型
24
形式验证 推理验证 模型检测 推理验证与模型检测相结合
25
推理验证+模型检测 int in() { char c=0; int k=0; while (1) { k=0; …
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { int in() { char c=0; int k=0; while (1) { k=0; … if (c=='\n') { return k; } return k; } k>=0; k<=20; 不可达 k>=0; k<=20;
26
推理验证+模型检测 int in() FUNCTION r=in() { ASSUMPTION TRUE; char c=0;
#include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { int in() { char c=0; int k=0; while (1) { k=0; … if (c=='\n') { return k; } return k; } FUNCTION r=in() ASSUMPTION TRUE; GUARANTEE r>=0&&r<=20; k>=0; k<=20; 不可达 k>=0; k<=20;
27
模型检测 时间优势对比: Time Time (with A/G) Model Checking 1233 205
./verds –c isr.c –sp isr.sp –fsp isr.fsp 时间优势对比: 验证结果 Time Time (with A/G) Model Checking 1233 205
28
验证过程 http://lcs.ios.ac.cn/~zwh/verds/ Automatic Translator C Program
Model VERDS Model Checker Specification Function Specification Positive Conclusion
29
模型检测的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的程序模型，如并发模型等 怎样提高效率
怎样增加其可应用性 怎样与其他方法结合以增加其可应用性
30
推理验证的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的程序模型，如并发模型等
怎样构造程序关键部位的关键性质 怎样增加其可应用性 怎样与其他方法结合以增加其可应用性
31
Questions?
Similar presentations
