Editing Model checking (section)

== Overview ==
Property checking is used for [[Software verification|verification]] when two descriptions are not equivalent. During [[Refinement (computing)|refinement]], the specification is complemented with details that are [[Don't-care term|unnecessary]] in the higher-level specification. There is no need to verify the newly introduced properties against the original specification since this is not possible. Therefore, the strict bi-directional equivalence check is relaxed to a one-way property check. The implementation or design is regarded as a model of the system, whereas the specifications are properties that the model must satisfy.<ref>{{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 |access-date=December 12, 2012|chapter=Chapter 1.1: What Is Design Verification?}}</ref>

An important class of model-checking methods has been developed for checking models of [[computer hardware|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".<ref>{{Cite web | url=http://amturing.acm.org/award_winners/pnueli_4725172.cfm/ | title=Amir Pnueli - A.M. Turing Award Laureate}}</ref>  Model checking began with the pioneering work of [[E. M. Clarke]], [[E. A. Emerson]],<ref name=Allen1980>{{citation
 | last1 = Allen Emerson | first1 = E.
 | last2 = Clarke | first2 = Edmund M.
 | title = Automata, Languages and Programming
 | chapter = Characterizing correctness properties of parallel programs using fixpoints
 | year = 1980
 | 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
 }}</ref><ref name="LoP81">Edmund M. Clarke, E. Allen Emerson: [http://portal.acm.org/citation.cfm?id=747438&dl= "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic"]. Logic of Programs 1981: 52-71.</ref><ref name=Clarke1986>{{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
| s2cid = 52853200
 | doi-access = free
 }}</ref> by J. P. Queille, and [[J. Sifakis]].<ref name=Queille1982>{{citation
 | last1 = Queille | first1 = J. P.
 | last2 = Sifakis | first2 = J.
 | title = International Symposium on Programming
 | chapter = Specification and verification of concurrent systems in CESAR
 | year = 1982
 | 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
 }}</ref> Clarke, Emerson, and Sifakis shared the 2007 [[Turing Award]] for their seminal work founding and developing the field of model checking.<ref>{{Cite web |url=http://www.acm.org/press-room/news-releases/turing-award-07/ |title=Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology |access-date=2009-01-06 |archive-url=https://web.archive.org/web/20081228210748/http://www.acm.org/press-room/news-releases/turing-award-07/ |archive-date=2008-12-28 |url-status=dead }}</ref><ref>[http://usacm.acm.org/usacm/weblog/index.php?p=572 ''USACM'': 2007 Turing Award Winners Announced]</ref>

Model checking is most often applied to hardware designs. For software, because of undecidability (see [[computability theory]]) the approach cannot be fully algorithmic, apply to all systems, and always give an answer; in the general case, it may fail to prove or disprove a given property. In [[embedded system|embedded-system]]s hardware, it is possible to validate a specification delivered, e.g., by means of [[UML activity diagram|UML activity diagrams]]<ref>{{Cite book | doi=10.1007/978-3-319-07013-1_22| chapter=Model Checking of UML Activity Diagrams in Logic Controllers Design| title=Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland| series=Advances in Intelligent Systems and Computing| year=2014| last1=Grobelna| first1=Iwona| last2=Grobelny| first2=Michał| last3=Adamski| first3=Marian| volume=286| pages=233–242| isbn=978-3-319-07012-4}}</ref> or control-interpreted [[Petri net]]s.<ref>I. Grobelna, "[https://www.researchgate.net/profile/Jan_Sikora3/publication/267037615_Advanced_Numerical_Modelling/links/5442adc40cf2e6f0c0f9366b/Advanced-Numerical-Modelling.pdf#page=63 Formal verification of embedded logic controller specification with computer deduction in temporal logic]", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47–50, 2011</ref>

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 [[vertex (graph theory)|vertices]]) and [[edge (graph theory)|edges]]. A set of atomic propositions is associated with each node, typically stating which memory elements are one. The [[Node (computer science)|nodes]] represent states of a system, the edges represent possible transitions that may alter the state, while the atomic propositions represent the basic properties that hold at a point of execution.<ref>{{FOLDOC|Model+checking}}</ref>

Formally, the problem can be stated as follows: given a desired property, expressed as a temporal logic formula <math>p</math>, and a structure <math>M</math> with initial state <math>s</math>, decide if <math>M,s \models p</math>.  If <math>M</math> is finite, as it is in hardware, model checking reduces to a [[graph search]].