电子学报 ›› 2002, Vol. 30 ›› Issue (S1): 1907-1912.
林惠民, 张文辉
收稿日期:
2002-08-16
修回日期:
2002-10-16
出版日期:
2002-12-25
作者简介:
基金资助:
国家自然科学基金 (No.6983320)
LIN Hui-min, ZHANG Wen-hui
Received:
2002-08-16
Revised:
2002-10-16
Online:
2002-12-25
Published:
2002-12-25
摘要: 随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题.在为此提出的诸多理论和方法中,模型检测(model checking)以其简洁明了和自动化程度高而引人注目.模型检测的研究大致涵盖以下内容:模态/时序逻辑、模型检测算法及其时空效率(特别是空间效率)的改进以及支撑工具的研制.这几个方面之间有着密切的内在联系.不同模态/时序逻辑的模型检测算法的复杂性不一样,优化算法往往是针对某些特定类型的逻辑公式.本文将就这几个方面分别加以阐述,最后介绍该领域的新进展.
中图分类号:
林惠民, 张文辉. 模型检测:理论、方法与应用[J]. 电子学报, 2002, 30(S1): 1907-1912.
LIN Hui-min, ZHANG Wen-hui . Model Checking: Theories, Techniques and Applications[J]. Acta Electronica Sinica, 2002, 30(S1): 1907-1912.
[1] E M Clarke,E A Emerson,A P Sistla.Automatic verification of finite state concurrent systems using temporal logic specifications[A].10th Annual ACM Symposium on Principles of Programming Languages (POPL 83)[C].New York:ACM Press,1983.117-126.[2] M Y Vardi,P Wolper.An automata-theoretic approach to automatic program verification[A].1st IEEE Symposium on Logic in Computer Science (LICS 86)[C].Los Alamitos:IEEE Computer Society,1986.322-331.[3] E Allen Emerson,Chin-Laung Lei.Efficient model checking in fragments of the propositional Mu-Calculus[A].1st IEEE Symposium on Logic in Computer Science (LICS 86)[C].Los Alamitos: IEEE Computer Society,1986.267-278.[4] Colin Stirling,David Walker.Local model checking in the modal Mu-Calculus[A].Lecture Notes in Computer Science 351-3rd International Joint Conference on Theory and Practice of Software Development (TAPSOFT 89)[C].Berlin: Springer-Verlag,1989.369-383.[5] Jorg Bormann,Jorg Lohse,Michael Payer,Gerd Venzl.Model checking in industrial hardware design[A].32nd Conference on Design Automation (DAC 95)[C].New York: ACM Press,1995.298-303.[6] Yirng-An Chen,Edmund M Clarke,Pei-Hsin Ho,Yatin Vasant Hoskote,Timothy Kam,Manpreet Khaira,John W O'Leary,Xudong Zhao.Verification of all circuits in a floating-point unit using word-level model checking[A].Lecture Notes in Computer Science 1166-1st International Conference on Formal Methods in Computer-Aided Design(FMCAD 96)[C].Berlin: Springer-Verlag,1996.19-33.[7] Gavin Lowe.Breaking and fixing the needham-schroeder public-key protocol using FDR[J].Software-Concepts and Tools,1996,17(3):93-102.[8] J C Mitchell,V Shmatikov,U Stern.Finite-state analysis of SSL 3.0[A].7th USENIX Security Symposium (USENIX 98)[C].Berkeley:USENIX,1998.201-215.[9] Paolo Maggi,Riccardo Sisto.Using SPIN to verify security properties of cryptographic protocols[A].Lecture Notes in Computer Science 2318-9th International SPIN Workshop on Model Checking of Software (SPIN 02)[C].Berlin: Springer-Verlag,2002.187-204.[10] Vitaly Shmatikov,John C Mitchell.Finite-state analysis of two contract signing protocols[J].Theoretical Computer Science,2002,283(2):419-450.[11] Edmund M Clarke,Orna Grumberg,Hiromi Hiraishi,Somesh Jha,David E Long,Kenneth L McMillan,Linda A Ness.Verification of the futurebus+ cache coherence protocol[J].Formal Methods in System Design,1995,6(2):217-232.[12] R J Anderson,P Beame,S Burns,W Chan,F Modugno,D Notkin,J D Reese.Model checking large software specifications[R].University of Washington,Department of Computer Science and Engineering.Report:TR-96-04-02,April,1996.[13] T Sreemani,J M Atlee.Feasibility of model checking software requirements[A].11th Annual Conference on Computer Assurance (COMPASS 96)[C].Gaithersburg,Maryland: National Institute of Standards and Technology,1996.[14] E Cleaveland,G Luttegen,V Natarajan,S Sims.Modeling and verifying distributed systems using priorities:A case study[J].Software Concepts and Tools,1996,17(2):50-62.[15] A Cimatti,F Giunchiglia,G Mongardi,D Romano,F Torielli,P Traverso.Model checking safety critical software with SPIN:an application to a railway interlocking system[A].Lecture Notes in Computer Science 1516-17th International Conference on Computer Safety,Reliability and Security(SAFECOMP 98)[C].Berlin:Springer-Verlag,1998.284-295.[16] Adam L Turk,Scott T Probst,Gary J Powers.Verification of real time chemical processing systems[A].Lecture Notes in Computer Science 1201-International Workshop on Hybrid and Real-Time Systems (HART 97)[C].Berlin: Springer-Verlag,1997.259-272.[17] Henk Eertink,Wil Janssen,Paul Oude Luttighuis,Wouter B Teeuw,Chris A Vissers. A business process design language[A].Lecture Notes in Computer Science 1708-World Congress on Formal Methods (FM 99)[C].Berlin: Springer-Verlag,1999.76-95.[18] Wenhui Zhang.Model checking operator procedures[A].Lecture Notes in Computer Science 1680-Theoretical and Practical Aspects of SPIN Model Checking(SPIN 99a,99b)[C].Berlin: Springer-Verlag,1999.200-215.[19] J R Burch,E M Clarke,K L McMillan,D L Dill,J Hwang.Symbolic model checking:1020 states and beyond[A].5th IEEE Symposium on Logic in Computer Science (LICS 90)[C].Los Alamitos: IEEE Computer Society,1990.428-439.[20] Randal E Bryant.Graph-based algorithms for boolean function manipulation[J].IEEE Transactions on Computers,1986,35(8):677-691.[21] G J Holzmann.Design and Validation of Computer Protocols[M].New Jersey:Prentice Hall,1991.[22] S Katz,D Peled.Verification of distributed programs using representative interleaving sequences[J].Distributed Computing,1992,6:107-120.[23] Gerard J Holzmann,Doron Peled.An improvement in formal verification[A].7th IFIP WG6.1 International Conference on Formal Description Techniques VII (FORTE 1994)[C].London: Chapman and Hall,1995.197-211.[24] E A Emerson,A P Sistla.Symmetry and model checking[A].Lecture Notes in Computer Science 697-5th International Conference on Computer Aided Verification (CAV 93)[C].Berlin: Springer-Verlag,1993.463-478.[25] A Prasad Sistla,Viktor Gyuris,E Allen Emerson.SMC:a symmetry-based model checker for verification of safety and liveness properties[J].ACM Transactions on Software Engineering and Methodology,2000,9(2):133-166.[26] Gerard J Holzmann,Anuj Puri.A minimized automaton representation of reachable states[J].International Journal on Software Tools for Technology Transfer,1999,2(3):270-278.[27] Patrick Cousot,Radhia Cousot.Systematic design of program analysis frameworks[A].6th Annual ACM Symposium on Principles of Programming Languages (POPL 79)[C].New York:ACM Press,1979.269-282.[28] E M Clarke,O Grumberg,D E Long.Model checking and abstraction[J].ACM Transactions on Programming Languages and Systems,1994,16(5):1512-1542.[29] C Loiseaux,S Graf,J Sifakis,A Bouajjani,S Bensalem.Property preserving abstractions for the verification of concurrent systems[J].Journal of Formal methods in System Design,1995,6:1-35.[30] Mark Weiser. Program slicing[J].IEEE Transactions on Software Engineering,1984,10(4):352-357.[31] Jingde Cheng.Slicing concurrent programs-a graph-theoretical approach[A].Lecture Notes in Computer Science 749-1st International Workshop on Automated and Algorithmic Debugging(AADEBUG 93)[C].Berlin: Springer-Verlag,1993.223-240.[32] L I Millett,T Teitelbaum.Issues in slicing PROMELA and its applications to model checking,protocol understanding,and simulation[J].International Journal on Software Tools for Technology Transfer,2000,2(4):343-349.[33] Eugene W Stark.A proof technique for rely/guarantee properties[A].Lecture Notes in Computer Science 206-5th Conference on Foundations of Software Technology and Theoretical Computer Science(FSTTCS 85)[C].Berlin: Springer-Verlag,1985.369-391.[34] E M Clarke,D E Long,K L McMillan.Compositional model checking[A].4th IEEE Symposium on Logic in Computer Science (LICS 89)[C].Los Alamitos: IEEE Computer Society,1989,353-362.[35] K Stahl,K Baukus,Y Lakhnech,M Steffen.Divide,abstract,and model-check[A].Lecture Notes in Computer Science 1680-Theoretical and Practical Aspects of SPIN Model Checking(SPIN 99a,99b)[C].Berlin: Springer-Verlag,1999.57-76.[36] K L McMillan.Symbolic model checking:an approach to the state explosion problem[R].Carnegie-Mellon University,Department of Computer Science, Report CMU-CS-92-131.1992.[37] G J Holzmann.The model checker SPIN[J].IEEE Transactions on Software Engineering,1997,23(5):279-295.[38] R Cleavel,J Parrow,B Steffen.The concurrency workbench:a semantics-based verification tool for the verification of concurrent systems[J].ACM Transactions on Programming Languages and Systems,1993,5(1):36-72.[39] Patrice Godefroid.VeriSoft: A tool for the automatic analysis of concurrent reactive software[A].Lecture Notes in Computer Science 1254-9th International Conference on Computer Aided Verification (CAV 97)[C].Berlin:Springer-Verlag,1997.476-479.[40] Bernd Walter.Timed Petri-nets for modelling and alalyzing protocols with real-time characteristics[A].3rd IFIP WG 6.1 International Workshop on Protocol Specification,Testing,and Verification (PSTV 83)[C].Amsterdam: North-Holland,1983.149-159.[41] James E Coolahan Jr,Nick Roussopoulos.A timed Petri net methodolgoy for specifying real-time system timing requirements[A].International Workshop on Timed Petri Nets (PNPM 85)[C].Los Alamitos:IEEE Computer Society,1985.24-31.[42] David L.Dill.Timing assumptions and verification of finite-state concurrent systems[A].Lecture Notes in Computer Science 407-International Workshop on Automatic Verification Methods for Finite State Systems (89)[C].Berlin: Springer-Verlag,1990.197-212.[43] Rajeev Alur,Costas Courcoubetis,David L Dill.Model-checking for Real-time systems[A].5ht IEEE Symposium on Logic in Computer Science (LICS 90)[C].Los Alamitos:IEEE Computer Society,1990.414-425.[44] Wang Yi.CCS+Time=An interleaving model for real time systems[A].Lecture Notes in Computer Science 510-18th International Colloquium on Automata,Languages and Programming(ICALP 91)[C].Berlin:Springer-Verlag,1991.217-228.[45] Steve Schneider,Jim Davies,D M Jackson,George M Reed,Joy N Reed,A W Roscoe.Timed CSP:theory and practice[A].Lecture Notes in Computer Science 600-Real-Time:Theory in Practice (REX Workshop 91)[C].Berlin:Springer-Verlag,1991.640-675.[46] E Allen Emerson,Aloysius K Mok,A Prasad Sistla,Jai Srinivasan.Quantitative temporal reasoning[A].Lecture Notes in Computer Science 531-2nd International Workshop on Computer Aided Verification (CAV 90)[C].Berlin: Springer-Verlag,1991.136-145.[47] Jonathan S Ostroff.Composition and refinement of discrte real-time systems[J].ACM Transactions on Software Engineering and Methodology,1999,8(1):1-48.[48] Thomas A.Henzinger,Xavier Nicollin,Joseph Sifakis,Sergio Yovine.Symbolic model checking for real-time systems[A].7th IEEE Symposium on Logic in Computer Science (LICS 92)[C].Los Alamitos:IEEE Computer Society,1992.394-406.[49] Kim G Larsen,Paul Pettersson,Wang Yi.UPPAAL in a nutshell[J].International Journal on Software Tools for Technology Transfer,1997,1(1-2):134-152.[50] Marius Bozga,Conrado Daws,Oded Maler,Alfredo Olivero,Stavros Tripakis,Sergio Yovine. KRONOS: A model-checking tool for real-time systems[A].Lecture Notes in Computer Science 1486-5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems(FTRTFT 98)[C].Berlin: Springer-Verlag,1998.298-302.[51] Nikolaj Bjorner,Anca Browne,Eddie Chang,Michael Colon,Arjun Kapur,Zohar Manna,Henny Sipma,Tomas Uribe.STeP-The Stanford Temporal Prover,User's Manual[R].Stanford University,Department of Computer Science,Report STAN-CS-TR-95-1562.1995.[52] Thomas A Henzinger,Pei-Hsin Ho,Howard Wong-Toi.HYTECH:A model checker for hybrid systems[A].Lecture Notes in Computer Science 1254-5th International Conference on Computer Aided Verification (CAV 97)[C].Berlin:Springer-Verlag,1997.460-463.[53] Richard H.Carver,Kuo-Chung Tai.Use of sequencing constraints for specification-based testing of concurrent programs[J].IEEE Transactions on Software Engineering,1998,24(6):471-490.[54] Klaus Havelund,John Penix,Willem Visser (eds).Lecture Notes in Computer Science 1885-7th International SPIN Workshop on SPIN Model Checking and Software Verification (SPIN 00)[C].Berlin: Springer-Verlag,2000.[55] Jamieson M Cobleigh,Lori A Clarke,Leon J Osterweil.FLAVERS-A finite state verification technique for software systems[J].IBM Systems Journal,2002,41(1):140-161.[56] M Hennessy,X Liu.A modal logic for message passing processes[J].Acta Informatica,1995,32(4):375-393.[57] J Rathke,M Hennessy.Local model checking for value-passing processes[A]. Lecture Notes in Computer Science 1281-3th International Sy-mposium on Theoretical Aspects of Computer Science (TACS 97)[C].Berlin:Springer-Verlag,1997.250-266.[58] Huimin Lin.Model checking value-passing processes[A].8th Asian Pacific Software Engineering Conference (APSEC 01)[C].Los Alamitos: IEEE Computer Society,2001.3-12.[59] M Dam.Model checking mobile processes[J].Information and Computation,1996,129: 35-51.[60] Luis Caires,Luca Cardeli.A spatial logic for concurrency (Part I)[A].Lecture Notes in Computer Science 2215-4th International Symposium on Theoretical Aspects of Computer Science (TACS 01)[C].Berlin: Springer-Verlag,2001.1-37. |
[1] | 王舜, 杜晔, 韩臻. 基于模块化Abstract-Refine算法框架的软件模型检测方法[J]. 电子学报, 2020, 48(5): 997-1002. |
[2] | 范艳焕, 李永明, 潘海玉. 不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 电子学报, 2018, 46(1): 152-159. |
[3] | 梁常建, 李永明. 具有模糊时态的广义可能性线性时序逻辑的模型检测[J]. 电子学报, 2017, 45(12): 2971-2977. |
[4] | 梁常建, 李永明. 广义可能性计算树逻辑的模型检测问题[J]. 电子学报, 2017, 45(11): 2641-2648. |
[5] | 朱维军, 周清雷, 李永亮. 以DNA为载体的线性时序逻辑模型检测[J]. 电子学报, 2016, 44(6): 1265-1271. |
[6] | 林运国, 雷红轩, 李永明. 量子马尔可夫链安全性模型检测[J]. 电子学报, 2014, 42(11): 2191-2197. |
[7] | 刘志锋, 孙博, 周从华. 概率实时时态认知逻辑模型检测中抽象技术的研究[J]. 电子学报, 2013, 41(7): 1343-1351. |
[8] | 周从华, 孙博, 刘志锋, 葛云. 概率时态认知逻辑模型检测中三值抽象技术的研究[J]. 电子学报, 2012, 40(10): 2052-2061. |
[9] | 王曦;徐中伟. 基于启发式SCCs的广义Büchi 自动机判空检测算法[J]. 电子学报, 2012, 40(1): 95-102. |
[10] | 张广泉;戎玫;朱雪阳;何亚丽;石慧娟. 基于XYZ/ADL的Web服务组合描述与验证[J]. 电子学报, 2011, 39(3A): 86-93. |
[11] | 尹传龙;庄雷;王从银;. 实时模型检测中基于驻留环的精确加速[J]. 电子学报, 2011, 39(3): 489-493. |
[12] | 张广泉;戎玫;王 Sheng. 时间感知Web服务交互行为建模与失配检测方法研究[J]. 电子学报, 2011, 39(11): 2568-2575. |
[13] | 王 雷;李 吉;李博洋. 缓冲区溢出漏洞精确检测方法研究[J]. 电子学报, 2008, 36(11): 2200-2204. |
[14] | 邵晨曦, 胡香冬, 熊焰, 蒋凡. 密码协议的SPIN建模和验证[J]. 电子学报, 2002, 30(S1): 2099-2101. |
阅读次数 | ||||||
全文 |
|
|||||
摘要 |
|
|||||