摘要: Model-checking gained wide popularity for analyzing software and hardware systems. However, even when the desired property holds, or model may still require fixing. For example, a ϕ: “on all paths, request is followed by an acknowledgment”, hold because no requests have been generated. Vacuity detection has proposed to address above problem. This technique able determine that ϕ satisfied vacuously in systems where are never sent. Recent work this area enabled computation of interesting witnesses satisfaction properties (in our case, those satisfy contain request) vacuity with respect subformulas single multiple subformula occurrences.
springer.com
core.ac.uk
sci-hub.st 参考文章(29)
Model Checking a Path (Preliminary Report) international conference on concurrency theory. ,vol. 2761, pp. 251- 265 ,(2003) , 10.1007/B11938
Michael Huth, Radha Jagadeesan, David Schmidt, Modal Transition Systems: A Foundation for Three-Valued Program Analysis european symposium on programming. pp. 155- 169 ,(2001) , 10.1007/3-540-45309-1_11
H. Rasiowa, Introduction to Metamathematics ,(1952)
Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh, Efficient Detection of Vacuity in ACTL Formulas computer aided verification. pp. 279- 290 ,(1997) , 10.1007/3-540-63166-6_28
Robin Milner, Bigraphical Reactive Systems international conference on concurrency theory. pp. 16- 35 ,(2001) , 10.1007/3-540-44685-0_2
Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh, Efficient Detection of Vacuity in Temporal Model Checking formal methods. ,vol. 18, pp. 141- 163 ,(2001) , 10.1023/A:1008779610539
Yifei Dong, Beata Sarna-Starosta, C. R. Ramakrishnan, Scott A. Smolka, Vacuity Checking in the Modal Mu-Calculus algebraic methodology and software technology. pp. 147- 162 ,(2002) , 10.1007/3-540-45719-4_11
Glenn Bruns, Patrice Godefroid, Model Checking with Multi-valued Logics Automata, Languages and Programming. pp. 281- 293 ,(2004) , 10.1007/978-3-540-27836-8_26
Glenn Bruns, Patrice Godefroid, Model Checking Partial State Spaces with 3-Valued Temporal Logics computer aided verification. pp. 274- 287 ,(1999) , 10.1007/3-540-48683-6_25
Marsha Chechik, Benet Devereux, Steve Easterbrook, Albert Y. C. Lai, Victor Petrovykh, Efficient Multiple-Valued Model-Checking Using Lattice Representations international conference on concurrency theory. pp. 441- 455 ,(2001) , 10.1007/3-540-44685-0_30