中国科学院软件研究所 计算机科学国家重点实验室 张文辉

Presentation on theme: "中国科学院软件研究所 计算机科学国家重点实验室 张文辉"— Presentation transcript:

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 程序的模型检测(例子)

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

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

12 反例分析 以下输入产生不正确结果 不正确运行

13 修正后的例子: 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:

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

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

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

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

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

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

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

22 并发模型的模型检测(例子)

23 并发模型的模型检测(例子) a=s0 b=t0 x=0 y=0 t=0

24 并发模型的模型检测 建模 验证问题 Model

25 并发模型(主程序) VVM VAR x: 0..1; y: 0..1; t: 0..1; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2&p1.b=t2)); AG((!p0.a=s1|AF(p0.a=s2|p1.b=t2))&(!p1.b=t1|AF(p0.a=s2|p1.b=t2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.b=t1|AF(p1.b=t2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.b=t1|EF(p1.b=t2)));

26 并发模型(进程模块说明1) MODULE p0m() VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1&(x=0|t=0): (a):=(s2); a=s1&!(x=0|t=0): (a):=(s1); a=s2: (y,a):=(0,s3); a=s2: (a):=(s2); a=s3: (y,t,a):=(1,1,s1);

27 并发模型(进程模块说明2) MODULE p1m() VAR b: {t0,t1,t2,t3}; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1&(y=0|t=1): (b):=(t2); b=t1&!(y=0|t=1): (b):=(t1); b=t2: (x,b):=(0,t3); b=t2: (b):=(t2); b=t3: (x,t,b):=(1,0,t1);

28 模型检测 ./verds -ck 1 me002.vvm VERSION: verds 1.42 - DEC 2012
FILE: me001.vvm PROPERTY: A G ! ((a = 2 )& (b = 2 )) bound = 1 time = 0 time = 0 bound = 2 time = 0 bound = 3 time = 0 bound = 4 time = 0 bound = 5 time = 0 bound = 6 time = 0 CONCLUSION: TRUE (time=0)

29 模型检测结论 Property Conclusion AG(!(p0.a=2&p1.a=2)) true
AG((!p0.a=1|AF(p0.a=2|p1.a=2))&(!p1.a=1|AF(p0.a=2|p1.a=2))) false AG((!p0.a=1|AF(p0.a=2))&(!p1.a=1|AF(p1.a=2))) AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

30 进程公平性说明

31 并发模型(主程序) VVM VAR x: 0..1; y: 0..1; t: 0..1; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2&p1.b=t2)); AG((!p0.a=s1|AF(p0.a=s2|p1.b=t2))&(!p1.b=t1|AF(p0.a=s2|p1.b=t2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.b=t1|AF(p1.b=t2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.b=t1|EF(p1.b=t2)));

32 并发模型(进程模块说明1a) MODULE p0m() VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1&(x=0|t=0): (a):=(s2); a=s1&!(x=0|t=0): (a):=(s1); a=s2: (y,a):=(0,s3); a=s2: (a):=(s2); a=s3: (y,t,a):=(1,1,s1); FAIRNESS running;

33 并发模型(进程模块说明2a) MODULE p1m() VAR b: {t0,t1,t2,t3}; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1&(y=0|t=1): (b):=(t2); b=t1&!(y=0|t=1): (b):=(t1); b=t2: (x,b):=(0,t3); b=t2: (b):=(t2); b=t3: (x,t,b):=(1,0,t1); FAIRNESS running;

34 模型检测结论 Property Conclusion AG(!(p0.a=2&p1.a=2)) true
AG((!p0.a=1|AF(p0.a=2|p1.a=2))&(!p1.a=1|AF(p0.a=2|p1.a=2))) AG((!p0.a=1|AF(p0.a=2))&(!p1.a=1|AF(p1.a=2))) false AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

35 进程公平性说明2

36 并发模型(主程序) VVM VAR x: 0..1; y: 0..1; t: 0..1; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2&p1.b=t2)); AG((!p0.a=s1|AF(p0.a=s2|p1.b=t2))&(!p1.b=t1|AF(p0.a=s2|p1.b=t2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.b=t1|AF(p1.b=t2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.b=t1|EF(p1.b=t2)));

37 并发模型(进程模块说明1b) MODULE p0m() VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1&(x=0|t=0): (a):=(s2); a=s1&!(x=0|t=0): (a):=(s1); a=s2: (y,a):=(0,s3); a=s2: (a):=(s2); a=s3: (y,t,a):=(1,1,s1); FAIRNESS running; a!=s2;

38 并发模型(进程模块说明2b) MODULE p1m() VAR b: {t0,t1,t2,t3}; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1&(y=0|t=1): (b):=(t2); b=t1&!(y=0|t=1): (b):=(t1); b=t2: (x,b):=(0,t3); b=t2: (b):=(t2); b=t3: (x,t,b):=(1,0,t1); FAIRNESS running; b!=t2;

39 模型检测结论 Property Conclusion AG(!(p0.a=2&p1.a=2)) true
AG((!p0.a=1|AF(p0.a=2|p1.a=2))&(!p1.a=1|AF(p0.a=2|p1.a=2))) AG((!p0.a=1|AF(p0.a=2))&(!p1.a=1|AF(p1.a=2))) AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

40 验证过程 http://lcs.ios.ac.cn/~zwh/verds/ 建模 验证问题 Model VERDS
Model Checker Positive Conclusion Negative Conclusion 安全性质 Error Trace

41 模型检测的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的模型 建立新方法 改建算法以增加可应用性
与其他方法结合以增加可应用性

42 模型检测的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的模型 建立新方法 改建算法以增加可应用性
与其他方法结合以增加可应用性 符号模型检测 限界模型检测 硬件/协议/软件 实时系统模型 概率系统模型 混成系统 抽象方法 反例制导抽象求精 偏序归约 对称技术 组合方法 推理方法

43 问题?