模型检测:理论、方法与应用

摘要/Abstract

摘要： 随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题.在为此提出的诸多理论和方法中,模型检测(model checking)以其简洁明了和自动化程度高而引人注目.模型检测的研究大致涵盖以下内容:模态/时序逻辑、模型检测算法及其时空效率(特别是空间效率)的改进以及支撑工具的研制.这几个方面之间有着密切的内在联系.不同模态/时序逻辑的模型检测算法的复杂性不一样,优化算法往往是针对某些特定类型的逻辑公式.本文将就这几个方面分别加以阐述,最后介绍该领域的新进展.

关键词: 系统可靠性, 模态/时序逻辑, 模型检测

Abstract: As computer hardware and software systems become more and more complex,how to assure the correctness and reliability of such system sbecomes an urgent problem. Among theories proposed as solutions to this problem, model checking has become a very attractive and appealing approach, because of its simplicity and high level of automation. Research on model checking covers the following subjects: modal/temporal logics, model checking algorithms, efficiency of model checking with respect to time and space(especially space complexity), and development of model checking tools. These aspects are closely related. Complexities of model checking algorithms vary very much for different modal/temporal logics, and optimizations are often targeted at certain types of logic fonnulas. Some new achievements and research directions are also discussed.

Key words: system reliability, modal/temporal logics, model checking

中图分类号:

TP311.1

林惠民, 张文辉. 模型检测:理论、方法与应用[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.