View source for Talk:Model checking

{{talkheader}}
{{WikiProject banner shell|class=C|1=
{{WikiProject Computing |importance=Low |science=yes |science-importance=High |software=yes |software-importance=Mid}}
}}
{{FOLDOC}}

== Only finite state spaces?? ==
"Model checking is a technique for automatically verifying correctness properties of ''finite-state'' systems." (emphasis as in original) I am a CS student and we are constantly doing model checking on infinite state systems, using the mCRL2 toolset. I am a bit confused why anyone would put this in here. One example I remember very clearly, and which trivially has an infinite state space, is given by process P = a.P.b + c, where you need an unbounded(!) counter to remember how many b actions you will have to do after you have done the c action. That is definately an infinite state space and you can model check it in mCRL2.
[[Special:Contributions/145.120.19.244|145.120.19.244]] ([[User talk:145.120.19.244|talk]]) 18:43, 14 May 2011 (UTC)

I agree that infinite state spaces should be mentioned, although the example mentioned above is perhaps not the best one (mCRL2 allows you to write this process down, but you can for instance not verify that after every 'a', a 'b' will eventually follow). However, with the use of abstraction techniques, one can verify infinite-state systems <ref>{{cite web|last1=Cranen|first1=S.|last2=Gazda|first2=M.W.|last3=Wesselink|first3=J.W.|last4=Willemse|first4=T.A.C.|title=Abstraction in Parameterised Boolean Equation Systems|url=http://alexandria.tue.nl/repository/books/749512.pdf}}</ref>. Also timed systems over a dense time domain can be viewed as infinite-state systems; there are various techniques to model check those. [[User:Scranen|Scranen]] ([[User talk:Scranen|talk]]) 10:56, 3 November 2014 (UTC)

----
I edit see also.. [[User:Taehoon|Taehoon]]

How are Moscow ML and Standard ML related to model-checking!? [[User:David.Monniaux|David.Monniaux]] 07:02, 23 Apr 2004 (UTC)

{{reflist-talk}}

== SMV article ==

I took the liberty in changing the SMV link from the existing "[[SMV|Selectable Mode Vocoder]]" to a yet nonexisting "[[Symbolic Model Checker]]" entry.
About Standard ML; as far as I know this is a programming language and thus not related to model checking. It has been, however, devised as a means to write down programs from algebraic specifications, but this does not relate to model checking (althought both are formal approaches towards generating better systems).

== Any Model Checking communities? ==

Does anyone know about communities, wikis, forums, mailinglists, newsgroups or other collaborative sites about model checking (or even formal verification)? Thanks for any kind of help. --[[User:Pintman|Marco Bakera]] 09:23, 14 April 2006 (UTC)

:There is a yahoo group for the timed model checker, [[Uppaal]], and there are alot of people in the industry in that group that might be able to point you from there, hopefully. --[[User:Ade1982|Ade1982]] 19:48, 7 August 2006 (UTC)

::Thanks for that hint. I'll try my best over there. --[[User:Pintman|Marco Bakera]] 10:37, 11 February 2007 (UTC)

:You may also want to take a look at [http://mcrl2.org/release/user_manual/support.html mCRL2] [[User:Scranen|Scranen]] ([[User talk:Scranen|talk]]) 10:59, 3 November 2014 (UTC)

== Model checking tools section ==

I have reverted the removal of the list of model checking tools. That the list is too extensive is IMO not sufficient for removing it altogether. Surely the list should better be consolidated or moved to a dedicated article. The links to other lists, unlike the links to the tools, could be removed or moved to See also section. Optionally, only major tools could be listed. Whatever is preferred, I find a complete removal unneeded. --[[User:Dan Polansky|Dan Polansky]] 16:42, 20 June 2007 (UTC)
: I have to agree, I was thinking myself of moving it to a dedicated list section, and then pointing to it, as it is far too long. I also would like to see the model-checkers categorised in some way, perhaps by the type of system they address (timed, untimed, hybrid), or by the specification language, or some other one. This should give the list some much needed structure.[[User:Ade1982|Ade1982]] 13:43, 21 June 2007 (UTC)
:: A first step might be to remove tools with no internal or external links. E.g., COSPAN was a historically important tool, but I don't believe it is any longer available for download or purchase (some version of its code may be part of the Cadence product). 
:: It would also be nice if the information provided for each tool were consistent. Some of the tools cite the software license, others give a high-level description of the tool's purpose, and others have no supporting information at all. 
:: I've removed HOL (which is a theorem prover, not a model checker) and SATABS (which is an abstraction tool and part of the CBMC toolchain). [[User:Clconway|Clconway]] ([[User talk:Clconway|talk]]) 18:39, 20 November 2007 (UTC)

== Renamed "model" to "structure" ==

The article says model checking checks whether a model satisfies a formula. My sources say it checks whether a structure satisfies (is a model of) a formula. I think both points of view on this totally trivial matter are perfectly correct, and I wouldn't be surprised to hear that both are widespread. In fact, when talking to colleagues I always say "model" for the general thing, without thinking of a theory that it is a model of.

But I am trying to make all the articles on model theory and related topics use consistent language, and since it's important to get universal algebra into the same boat, Hodges' terminology seems to be most acceptable. It seems he put a lot of effort into getting the terminology right so it's acceptable to everybody. I hope nobody is offended by this change. --[[User:Hans Adler|Hans Adler]] ([[User talk:Hans Adler|talk]]) 01:49, 20 November 2007 (UTC)
:I think (although I do not have any written source) the notational ambiguity arising here is that "model" may refer either to the result of '''mathematical modelling''' a real-world system, or to a (say) [[Kripke structure]] that '''models''' some logical formula. I think that indeed the "model" in model checking refers to the first meaning, that is: we verify a simplified mathematical model instead of the whole system as it is. Is anyone aware of the original paper where the term "model checking" was coined? [[User:Hermel|Hermel]] ([[User talk:Hermel|talk]]) 15:36, 7 January 2009 (UTC)
::Clarke http://www.model.in.tum.de/um/25/pdf/Clarke.pdf writes: "We used the term Model Checking because we wanted to determine if the temporal formula f was true in the Kripke structure M, i.e., whether the structure M was a model for the formula f. Some people believe erroneously that the use of the term "model" refers to the dictionary meaning of this word (e.g., a miniature representation of something or a pattern of something to be made) and indicates that we are dealing with an abstraction of the actual system under study." (For fair credit: I've just happened to learn this reference from a Japanese colleague's blog http://yoriyuki-jp.blogspot.jp/2012/06/blog-post_17.html and decided to check English Wikipedia.) [[Special:Contributions/130.34.188.206|130.34.188.206]] ([[User talk:130.34.188.206|talk]]) 00:35, 18 June 2012 (UTC)

== List of External Links ==

I'm moving this list of links here from the main article, because the article is ungainly in its current form. Probably all of these (or nearly all) should just be deleted per [[WP:LINKFARM]]. [[User:Clconway|Clconway]] ([[User talk:Clconway|talk]]) 15:43, 6 January 2009 (UTC)
:Please refrain from adding your favorite model checking tools to the list of external links in the article without justifying at this talk page the importance of your tool over others. AFTER the community has agreed about the most notable/commonly used ones, we can add them to the article. Otherwise we will end up with a linkfarm as we had it before. Any objections to this process? [[User:Hermel|Hermel]] ([[User talk:Hermel|talk]]) 08:37, 19 January 2009 (UTC)  

;Model checking tools
*[http://www.inrialpes.fr/vasy/cadp/ CADP - Construction and Analysis of Distributed Processes]
*[http://www.cs.cmu.edu/~modelcheck/cbmc/ CBMC] - a bounded model checker for C/C++ programs
*[http://divine.fi.muni.cz/  DiVinE - Distributed Verification Environment]
*[http://www.osc-es.de/index.php?lang=2&idcat=18 '''EmbeddedValidator''', The Matlab/Simulink/Stateflow/Targetlink Formal Verification Environment]
*[http://www.dsi.uniroma1.it/~tronci/cached.murphi.html FHP-Murphi] - Finite Horizon Probabilistic Murphi
*[http://jabc.cs.uni-dortmund.de/modelchecking/ GEAR], a game based model checking tool capable of [[Computational tree logic|CTL]], [[modal mu calculus|modal µ-calculus]] and [http://patterns.projects.cis.ksu.edu/ specification patterns].
* [http://helena.cnam.fr/ Helena] — High Level Colored Petri Nets Analyzer
*[http://www.montefiore.ulg.ac.be/~boigelot/research/lash/ LASH], Liège Automata-based Symbolic Handler
*[http://www.doc.ic.ac.uk/ltsa/ LTSA], Labelled Transition System Analyser -- Imperial College, London
*[http://www-i11.informatik.rwth-aachen.de/mc_square.html <nowiki>[mc]square</nowiki>], a model checker for microcontroller (ATMEL ATmega and Infineon XC167) assembly code
*[http://www.fmi.uni-stuttgart.de/szs/tools/moped/ MOPED]
*[http://www.cs.berkeley.edu/~daw/mops/ MOPS], Modelchecking Programs for Security properties
*[http://www.dsi.uniroma1.it/~tronci/cached.murphi.html CMurphi] Caching Murphi
*[http://homepages.cwi.nl/~mcrl/ μCRL], [[GNU General Public License|GPL]], Based on [[Algebra of Communicating Processes|ACP]]
*[http://www.mcrl2.org/ mCRL2 Toolset], [[Boost Software License]], Based on [[Algebra of Communicating Processes|ACP]]
*[http://www.stlab.dsi.unifi.it/oris/ ORIS], uses a [[Computational tree logic|CTL]]-like temporal logic with real-time bounds, action and state based.
*[http://www.ecs.soton.ac.uk/~mal/systems/prob.html ProB]
*[http://www.cs.bham.ac.uk/~dxp/prism/ PRrobabilistIc Symbolic Model checker (PRISM)]
*[http://www.lemma-one.com/ProofPower/index/ ProofPower]
*[http://www.dcs.gla.ac.uk/prosper/ PROSPER] - a formal design tool that incorporates model checking
*[http://www.prover.com/products/PPI Prover Plug-In commercial proof engines]
*[http://www-ti.informatik.uni-tuebingen.de/~fmg/raven/raven.html RAVEN (Real-Time Analysis and Verification Environment)]
*[http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/ RuleBase]
*[http://research.microsoft.com/slam/ SLAM] and [http://www.microsoft.com/whdc/devtools/tools/SDV.mspx Static Driver Verifier (SDV)] - CEGAR-style model checking for systems code
*[http://www.cs.cmu.edu/~modelcheck/smv.html Symbolic Model Checker (SMV)], the original symbolic model checker
*[http://www.osc-es.de/index.php?lang=2&idcat=19 '''Statemate ModelChecker''', Statemate Models Robustness Checking]
*[http://www.osc-es.de/index.php?lang=2&idcat=20 '''Statemate ModelCertifier''', Statemate Models Requirements Certification]
*[http://statestep.com Statestep] Specification and modeling tool; checks that invalid states are not reachable.
*[http://steam.cs.uni-dortmund.de/index.html StEAM (State Exploring Assemblylevel Model Checker)] Verification of concurrent C++ programs
*[http://www.veromodo.com/tempo/ TEMPO] Modeling and verification environment for realtime and hybrid systems
*[http://research.microsoft.com/users/lamport/tla/tlc.html TLC]
*[http://cs.nyu.edu/acsys/tlv/index.html Temporal Logic Verifier (TLV)]
*[http://research.microsoft.com/TERMINATOR Terminator] Verification of termination and other [[liveness]] properties for the C programming language 
*[http://www.uppaal.com Uppaal Model Checker (UPPAAL)]
*[http://www.cs.cmu.edu/~modelcheck/vcegar Model checker for Verilog based on CEGAR (VCEGAR)]
*[http://vlsi.colorado.edu/~vis/ Verification Interacting with Synthesis (VIS)]

;Other
*[http://anna.fi.muni.cz/yahoda/ Database of Verification and Model Checking Tools] (Yahoda)

;Research groups
*[http://www.facweb.iitkgp.ernet.in/~pallab/forverif.html ''Formal-V group — Indian Institute Of Technology, Kharagpur, India'']
*[http://uclid.eecs.berkeley.edu ''UCLID group at UC Berkeley'']
*[http://sdg.csail.mit.edu/ ''Software Design Group at MIT'']
*[http://www.itc.it/irst/Renderer.aspx?targetID=252 ''Automated Reasoning Systems (SRA) -  at Bruno Kessler Foundation, Trento Italy'']
*[http://www.cs.bham.ac.uk/research/labs/modelling_and_analysis_of_systems/ ''Modelling and Analysis of Complex Systems group at The University of Birmingham, England'']
*[http://www-i2.informatik.rwth-aachen.de ''Software Modeling and Verification (MOVES) group  at RWTH Aachen University, Germany'']
*[http://fmt.cs.utwente.nl ''Formal Methods & Tools (FMT) group at The University of Twente, The Netherlands'']
*[http://www-2.cs.cmu.edu/~modelcheck/ ''Model Checking at Carnegie Mellon University'']
*[http://svvat.ece.utexas.edu/ ''Software Verification and Validation at UT Austin'']
*[http://www.cis.ksu.edu/santos/ ''SAnToS Laboratory at K-State'']
*[http://ase.arc.nasa.gov/ ''Automated Software Engineering at Nasa Ames Research Center'']
*[http://eis.jpl.nasa.gov/lars/ ''NASA/JPL Laboratory for Reliable Software'']
*[http://vlsi.colorado.edu/ ''VLSI/CAD Research group — University of Colorado at Boulder'']
*[http://www.cs.utah.edu/formal_verification/ ''Formal Methods Research Group, University of Utah '']
*[http://vv.cs.byu.edu/ ''Verification and Validation — Brigham Young University, Provo, Utah'']
*[http://www.fi.muni.cz/paradise/ ''ParaDiSe Laboratory — Masaryk University in Brno'']
*[http://www.inrialpes.fr/vasy ''VASY Research team — INRIA Rhône-Alpes, France'']
*[http://smv.unige.ch ''Software Modeling and Verification (SMV) group — University of Geneva (Switzerland)'']

== Why link yet another two mc tools ==

I removed the following links:

;tools
* [http://www.computer.org/portal/web/csdl/doi/10.1109/TSE.2008.104 '''Charmy''', CHARMY: A Framework for Designing and Verifying Architectural Specifications]

;External link
* [http://www.rkbexplorer.com/explorer/#display=mechanism-{http://resex.rkbexplorer.com/id/resilience-mechanism-0a4a4dc0} Model checking in the RKBExplorer]

because the community has never discussed either CHARMY or RKBExplorer. Moreover the first one links to a paper, not to CHARMY wiki pages.

[[User:PoorUser|PoorUser]] ([[User talk:PoorUser|talk]]) 13:01, 22 October 2009 (UTC)

== Merge here: [[Temporal logic in finite-state verification]] ==

I suggest we merge [[Temporal logic in finite-state verification]] into [[Model checking]]. Since its last AfD four years ago, and since 2011 when the article was tagged with the "essay-like style" issue and a merger suggestion, no significant changes have been made. I believe the last AfD failed because the participants were mainly non-experts but all of the information discussed is already covered at [[model checking]], [[formal verification]] or [[linear temporal logic]], bar the specific example given in the article, which I believe we can usefully merge to [[Model checking]]. This is not a meaningfully different scope for an article than those three articles and as such has no scope for growth that would not be best targeted instead at improving those articles. — [[User:Bilorv|Bilorv]] ('''[[User talk:Bilorv|<span style="color:purple">talk</span>]]''') 22:52, 15 July 2020 (UTC)
:{{agree}} - [[User:Jochen Burghardt|Jochen Burghardt]] ([[User talk:Jochen Burghardt|talk]]) 12:37, 16 July 2020 (UTC)
::Alright, thanks for the reply. It's been about a week and there's no opposition so I've gone and merged it. If anyone objects then they can revert and then we can discuss further. — [[User:Bilorv|Bilorv]] ('''[[User talk:Bilorv|<span style="color:purple">talk</span>]]''') 17:21, 21 July 2020 (UTC)

== Link "The Beginning of Model Checking: A Personal Perspective" does not work ==

The Link to "The Beginning of Model Checking: A Personal Perspective" in the section "further reading" seems to be outdated. I do not know, how such thing should be handled. Maybe change link to the following page: [https://link.springer.com/chapter/10.1007/978-3-540-69850-0_2 Springer web page].
--[[User:JonathenHarker|JonathenHarker]] ([[User talk:JonathenHarker|talk]]) 12:26, 13 December 2020 (UTC)

:Thanks for noticing, and for the link. I made it a <nowiki>{{cite book}}</nowiki> entry. In general, if you find an external link that doesn't work, just append <nowiki>{{deadlink}}</nowiki>, and hope that someone will fix it; if you already have a better link, just replace the old one. - [[User:Jochen Burghardt|Jochen Burghardt]] ([[User talk:Jochen Burghardt|talk]]) 13:07, 13 December 2020 (UTC)