中国科学院软件研究所 计算机科学国家重点实验室 张文辉 http://lcs.ios.ac.cn/~zwh/ 中国科学院研究生院信息科学与工程学院课程 程序的形式验证 – 简介 中国科学院软件研究所 计算机科学国家重点实验室 张文辉 http://lcs.ios.ac.cn/~zwh/

程序正确性的重要性 应用广泛 软件错误的可能后果 航空 航天 金融 设备的控制 日常生活 火箭 Ariane 5 Explosion (1997) 火星气候轨道器 NASA Mars Climate Orbiter (1999)

程序正确性方法 测试 形式验证 黑盒测试 白盒测试 推理验证 模型检测 可执行代码 程序代码 程序代码或其抽象模型 程序运行环境模型 规则 算法

例子: 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: 2 RESULT: 1   N: 10 RESULT: 3 N: 20 RESULT: 4 N: 30 INFO: the input number must be in {0,...,20} N: 5 RESULT: 2 N:

例子: 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之间的整数时， 输出为其平方根的整数部分。

测试 黑盒测试 白盒测试 Program testing can be used to show the presence of bugs, but never to show their absence! -- Edsger W. Dijkstra

形式验证 推理验证 模型检测 正确性 正确性+不正确性

例子: 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)

模型检测 ./verds –c isr.c –sp isr.sp 验证结果 反例

验证过程 Automatic Translator C Program Model VERDS Model Checker Specification Negative Conclusion Error Trace

反例分析 以下输入产生不正确结果 1 3 5 7 9 11 13 15 17 19 0 2 4 6 8 10 12 14 16 18 4 不正确运行

修正后的例子: 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: 2 RESULT: 1   N: 10 RESULT: 3 N: 20 RESULT: 4 N: 30 INFO: the input number must be in {0,...,20} N: 5 RESULT: 2 N:

模型检测 ./verds –c isr2.c –sp isr.sp 验证结果

验证过程 Automatic Translator C Program Model VERDS Model Checker Specification Positive Conclusion

模型检测的缺点与优点 缺点 可直接验证的程序规模小 可直接验证的程序结构简单 优点: 自动验证 对不正确的程序可生成诊断信息

推理验证 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); }

推理验证 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);

推理验证(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;

推理验证(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;

推理验证(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);

推理验证 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);

推理验证 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);

推理验证的缺点与优点 缺点 原则上不能自动化 验证人员需要知道程序关键部位的关键性质 对确认程序的不正确难度大 优点 可验证任意规模的模型

形式验证 推理验证 模型检测 推理验证与模型检测相结合

推理验证+模型检测 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;

推理验证+模型检测 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;

模型检测 时间优势对比: 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

验证过程 http://lcs.ios.ac.cn/~zwh/verds/ Automatic Translator C Program Model VERDS Model Checker Specification Function Specification Positive Conclusion http://lcs.ios.ac.cn/~zwh/verds/

模型检测的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的程序模型，如并发模型等 怎样提高效率 怎样增加其可应用性 怎样与其他方法结合以增加其可应用性

推理验证的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的程序模型，如并发模型等 怎样构造程序关键部位的关键性质 怎样增加其可应用性 怎样与其他方法结合以增加其可应用性

Questions?