词条 | Model checking |
释义 |
In computer science, model checking or property checking refers to the following problem: Given a model of a system, exhaustively and automatically check whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems. In order to solve such a problem algorithmically, both the model of the system and the specification are formulated in some precise mathematical language. To this end, the problem is formulated as a task in logic, namely to check whether a given structure satisfies a given logical formula. This general concept applies to many kinds of logics and suitable structures. A simple model checking problem is verifying whether a given formula in the propositional logic is satisfied by a given structure. OverviewProperty checking is used for verification instead of equivalence checking when two descriptions are not functionally equivalent. Particularly, during refinement, the specification is complemented with the details that are unnecessary in the higher level specification. Yet, there is no need to verify the newly introduced properties against the original specification. It is not even possible. Therefore, the strict bi-directional equivalence check is relaxed to one-way property checking. The implementation or design is regarded a model of the circuit whereas the specifications are properties that the model must satisfy.[1] An important class of model checking methods have been developed for checking models of hardware and software designs where the specification is given by a temporal logic formula. Pioneering work in temporal logic specification was done by Amir Pnueli, who received the 1996 Turing award for "seminal work introducing temporal logic into computing science".[2] Model checking began with the pioneering work by E. M. Clarke and E. A. Emerson[3][4][5] and by J. P. Queille and J. Sifakis.[6] Clarke, Emerson, and Sifakis shared the 2007 Turing Award for their seminal work founding and developing the field of model checking.[7][8] Model checking is most often applied to hardware designs. For software, because of undecidability (see computability theory) the approach cannot be fully algorithmic; typically it may fail to prove or disprove a given property. In embedded systems hardware designs it is possible to validate (verify against some specified requirements) a specification delivered i.e. by means of UML activity diagrams[9] or control interpreted Petri nets.[10] The structure is usually given as a source code description in an industrial hardware description language or a special-purpose language. Such a program corresponds to a finite state machine (FSM), i.e., a directed graph consisting of nodes (or vertices) and edges. A set of atomic propositions is associated with each node, typically stating which memory elements are one. The nodes represent states of a system, the edges represent possible transitions which may alter the state, while the atomic propositions represent the basic properties that hold at a point of execution. Formally, the problem can be stated as follows: given a desired property, expressed as a temporal logic formula p, and a structure M with initial state s, decide if . If M is finite, as it is in hardware, model checking reduces to a graph search. Algorithmsstate space enumeration, symbolic state space enumeration, abstract interpretation, symbolic simulation, symbolic trajectory evaluation, symbolic executionExplicit-state model checking{{Expand section|date=January 2011}}Symbolic model checking{{Expand section|date=January 2011}}Instead of enumerating reachable states one at a time, the state space can sometimes be traversed more efficiently by considering large numbers of states at a single step. When such state space traversal is based on representations of set of states and transition relations as logical formulas, binary decision diagrams (BDD) or other related data structures, the model-checking method is symbolic. Historically, the first symbolic methods used BDDs. After the success of propositional satisfiability in solving the planning problem in artificial intelligence (see satplan) in 1996, the same approach was generalized to model checking for the Linear Temporal Logic LTL (the planning problem corresponds to model-checking for safety properties). This method is known as bounded model checking.[11] The success of Boolean satisfiability solvers in bounded model checking led to the widespread use of satisfiability solvers in symbolic model checking.[12] TechniquesModel checking tools face a combinatorial blow up of the state-space, commonly known as the state explosion problem, that must be addressed to solve most real-world problems. There are several approaches to combat this problem.
Model checking tools were initially developed to reason about the logical correctness of discrete state systems, but have since been extended to deal with real-time and limited forms of hybrid systems. Tools{{main|List of model checking tools}}Here is a partial list of model checking tools that have a Wikipedia page:
See also
References{{Refimprove|date=November 2008}}{{commons category|Model checking (computer science)}}1. ^{{cite book |last= Lam K.|first=William |year=2005 |title=Hardware Design Verification: Simulation and Formal Method-Based Approaches |chapter-url=http://my.safaribooksonline.com/book/electrical-engineering/semiconductor-technology/0131433474/an-invitation-to-design-verification/ch01lev1sec1#X2ludGVybmFsX0h0bWxWaWV3P3htbGlkPTAxMzE0MzM0NzQlMkZjaDAxbGV2MXNlYzEmcXVlcnk9 |accessdate=December 12, 2012|chapter=Chapter 1.1: What Is Design Verification?}} 2. ^{{Cite web | url=http://amturing.acm.org/award_winners/pnueli_4725172.cfm/ | title=Amir Pnueli - A.M. Turing Award Laureate}} 3. ^{{citation | last1 = Allen Emerson | first1 = E. | last2 = Clarke | first2 = Edmund M. | year = 1980 | title = Characterizing correctness properties of parallel programs using fixpoints | journal = Automata, Languages and Programming | volume = 85 | pages = 169–181 | doi = 10.1007/3-540-10003-2_69| series = Lecture Notes in Computer Science | isbn = 978-3-540-10003-4 }} 4. ^Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic". Logic of Programs 1981: 52-71. 5. ^{{citation | last1 = Clarke | first1 = E. M. | last2 = Emerson | first2 = E. A. | last3 = Sistla | first3 = A. P. | year = 1986 | title = Automatic verification of finite-state concurrent systems using temporal logic specifications | journal = ACM Transactions on Programming Languages and Systems | volume = 8 | pages = 244 | doi = 10.1145/5397.5399 | issue = 2}} 6. ^{{citation | last1 = Queille | first1 = J. P. | last2 = Sifakis | first2 = J. | year = 1982 | title = Specification and verification of concurrent systems in CESAR | journal = International Symposium on Programming | volume = 137 | pages = 337–351 | doi = 10.1007/3-540-11494-7_22| series = Lecture Notes in Computer Science | isbn = 978-3-540-11494-9 }} 7. ^Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology 8. ^USACM: 2007 Turing Award Winners Announced 9. ^I. Grobelna, M. Grobelny, M. Adamski, "Model Checking of UML Activity Diagrams in Logic Controllers Design", Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX, Advances in Intelligent Systems and Computing Volume 286, Springer International Publishing Switzerland, pp. 233–242, 2014 10. ^I. Grobelna, "Formal verification of embedded logic controller specification with computer deduction in temporal logic", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47–50, 2011 11. ^{{Cite journal | last1 = Clarke | first1 = E. | last2 = Biere | first2 = A. | last3 = Raimi | first3 = R. | last4 = Zhu | first4 = Y. | journal = Formal Methods in System Design | volume = 19 | pages = 7–34 | year = 2001 | doi = 10.1023/A:1011276507260|title=Bounded Model Checking Using Satisfiability Solving}} 12. ^{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | pages = 2021–2035 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=Boolean Satisfiability Solvers and Their Applications in Model Checking}} 13. ^* Symbolic Model Checking, Kenneth L. McMillan, Kluwer, {{ISBN|0-7923-9380-5}}, also online. 14. ^{{cite web |url=https://www.cs.rice.edu/~lm30/RSynth/CUDD/cudd/doc/ |title=CUDD: CU Decision Diagram Package }} 15. ^{{cite web |url=http://vlsicad.eecs.umich.edu/BK/Slots/cache/www.itu.dk/research/buddy/ |title=BuDDy – A Binary Decision Diagram Package}} 16. ^{{citation | last1 = Clarke | first1 = Edmund | last2 = Grumberg | first2 = Orna | last3 = Jha | first3 = Somesh | last4 = Lu | first4 = Yuan | last5 = Veith | first5 = Helmut | year = 2000 | title = Counterexample-Guided Abstraction Refinement | journal = Computer Aided Verification | volume = 1855 | pages = 154–169 | doi = 10.1007/10722167_15| series = Lecture Notes in Computer Science | isbn = 978-3-540-67770-3 }} 17. ^[https://www.microsoft.com/en-us/research/project/zing Zing] Further reading
2 : Model checking|Logic in computer science |
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。