【正文】 char c=0。 int k=0。 while (1) { k=0。 … if (c==39。\n39。) { return k。 } … return k。 } } k=0。 k=20。 不可達(dá) k=0。 k=20。 FUNCTION r=in() ASSUMPTION TRUE。 GUARANTEE r=0amp。amp。r=20。 模型檢測(cè) ./verds –c –sp –fsp 時(shí)間優(yōu)勢(shì)對(duì)比 : 驗(yàn)證結(jié)果 Time Time (with A/G) Model Checking 1233 205 驗(yàn)證過(guò)程 C Program Model Automatic Translator VERDS Model Checker Specification Positive Conclusion Function Specification 并發(fā)模型的模型檢測(cè) (例子 ) 并發(fā)模型的模型檢測(cè) (例子 ) a=s0 b=t0 x=0 y=0 t=0 并發(fā)模型的模型檢測(cè) 驗(yàn)證問(wèn)題 Model 建模 并發(fā)模型 (主程序 ) 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(!(=s2amp。=t2))。 AG((!=s1|AF(=s2|=t2))amp。(!=t1|AF(=s2|=t2)))。 AG((!=s1|AF(=s2))amp。(!=t1|AF(=t2)))。 AG((!=s1|EF(=s2))amp。(!=t1|EF(=t2)))。 并發(fā)模型 (進(jìn)程模塊說(shuō)明 1) MODULE p0m() VAR a: {s0,s1,s2,s3}。 INIT a=s0。 TRANS a=s0: (y,t,a):=(1,1,s1)。 a=s1amp。(x=0|t=0): (a):=(s2)。 a=s1amp。!(x=0|t=0): (a):=(s1)。 a=s2: (y,a):=(0,s3)。 a=s2: (a):=(s2)。 a=s3: (y,t,a):=(1,1,s1)。 并發(fā)模型 (進(jìn)程模塊說(shuō)明 2) MODULE p1m() VAR b: {t0,t1,t2,t3}。 INIT b=t0。 TRANS b=t0: (x,t,b):=(1,0,t1)。 b=t1amp。(y=0|t=1): (b):=(t2)。 b=t1amp。!(y=0|t=1): (b):=(t1)。 b=t2: (x,b):=(0,t3)。 b=t2: (b):=(t2)。 b=t3: (x,t,b):=(1,0,t1)。 模型檢測(cè) ./verds ck 1 VERSION: verds DEC 2020 FILE: PROPERTY: A G ! ((a = 2 )amp。 (b = 2 )) bound = 1 time = 0 time = 0 bound = 2 time = 0 time = 0 bound = 3 time = 0 time = 0 bound = 4 time = 0 time = 0 bound = 5 time = 0 time = 0 bound = 6 time = 0 time = 0 CONCLUSION: TRUE (time=0) 模型檢測(cè)結(jié)論 Property Conclusion AG(!(=2amp。=2)) true AG((!=1|AF(=2|=2))amp。(!=1|AF(=2|=2))) false AG((!=1|AF(=2))amp。(!=1|AF(=2))) false AG((!=1|EF(=2))amp。(!=1|EF(=2))) true 進(jìn)程公平性說(shuō)明 并發(fā)模型 (主程序 ) 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(!(=s2amp。=t2))。 AG((!=s1|AF(=s2|=t2))amp。(!=t1|AF(=s2|=t2)))。 AG((!=s1|AF(=s2))amp。(!=t1|AF(=t2)))。 AG((!=s1|EF(=s2))amp。(!=t1|EF(=t2)))。 并發(fā)模型 (進(jìn)程模塊說(shuō)明 1a) MODULE p0m() VAR a: {s0,s1,s2,s3}。 INIT a=s0。 TRANS a=s0: (y,t,a):=(1,1,s1)。 a=s1amp。(x=0|t=0): (a):=(s2)。 a=s1amp。!(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。 并發(fā)模型 (進(jìn)程模塊說(shuō)明 2a) MODULE p1m() VAR b: {t0,t1,t2,t3}。 INIT b=t0。 TRANS b=t0: (x,t,b):=(1,0,t1)。 b=t1amp。(y=0|t=1): (b):=(t2)。 b=t1amp。!(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。 模型檢測(cè)結(jié)論 Property Conclusion AG(!(=2amp。=2)) true AG((!=1|AF(=2|=2))amp。(!=1|AF(=2|=2))) true AG((!=1|AF(=2))amp。(!=1|AF(=2))) false AG((!=1|EF(=2))amp。(!=1|EF(=2))) true 進(jìn)程公平性說(shuō)明 2 并發(fā)模型 (主程序 ) 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(!(=s2amp。=t2))。 AG((!=s1|AF(=s2|=t2))amp。(!=t1|AF(=s2|=t2)))。 AG((!=s1|AF(=s2))amp。(!=t1|AF(=t2)))。 AG((!=s1|EF(=s2))amp。(!=t1|EF(=t2)))。 并發(fā)模型 (進(jìn)程模塊說(shuō)明 1b) MODULE p0m() VAR a: {s0,s1,s2,s3}。 INIT a=s0。 TRANS a=s0: (y,t,a):=(1,1,s1)。 a=s1amp。(x=0|t=0): (a):=(s2)。 a=s1amp。!(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。 并發(fā)模型 (進(jìn)程模塊說(shuō)明 2b) MODULE p1m() VAR b: {t0,t1,t2,t3}。 INIT b=t0。 TRANS b=t0: (x,t,b):=(1,0,t1)。 b=t1amp。(y=0|t=1): (b):=(t2)。 b=t1amp。!(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。 模型檢測(cè)結(jié)論 Property Conclusion AG(!(=2amp。=2)) true AG((!=1|AF(=2|=2))amp。(!=1|AF(=2|=2))) true AG((!=1|AF(=2))amp。(!=1|AF(=2))) true AG((!=1|EF(=2))amp。(!=1|EF(=2))) true 驗(yàn)證過(guò)程 驗(yàn)證問(wèn)題 Model 建模 VERDS Model Checker Positive Conclusion Negative Conclusion Error Trace 安全性質(zhì) 模型檢測(cè)的學(xué)習(xí)與研究 ? 學(xué)習(xí) –原理 –相關(guān)知識(shí) ? 應(yīng)用 –將其應(yīng)用于一些簡(jiǎn)單程序 –將其應(yīng)用于不同類型的模型 ? 研究 –建立新方法 –改建算法以增加可應(yīng)用性 –與其他方法結(jié)合以增加可應(yīng)用性 模型檢測(cè)的學(xué)習(xí)與研究 ? 學(xué)習(xí) –原理 –相關(guān)知識(shí) ? 應(yīng)用 –將其應(yīng)用于一些簡(jiǎn)單程序 –將其應(yīng)用于不同類型的模型 ? 研究 –建立新方法 –改建算法以增加可應(yīng)用性 –與其他方法結(jié)合以增加可應(yīng)用性 抽象方法 反例制導(dǎo)抽象求精 偏序歸約 對(duì)稱技術(shù) 組合方法 推理方法 符號(hào)模型檢測(cè) 限界模型檢測(cè) 硬件 /協(xié)議 /軟件 實(shí)時(shí)系統(tǒng)模型 概率系統(tǒng)模型 混成系統(tǒng) 問(wèn)題 ?