Talk:Model checking

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. 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 . Also timed systems over a dense time domain can be viewed as infinite-state systems; there are various techniques to model check those. Scranen (talk) 10:56, 3 November 2014 (UTC)

---

I edit see also.. Taehoon

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

References

SMV article

I took the liberty in changing the SMV link from the existing "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. --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. --Ade1982 19:48, 7 August 2006 (UTC)

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

You may also want to take a look at mCRL2 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. --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.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). 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. --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? 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.) 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. 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? Hermel (talk) 08:37, 19 January 2009 (UTC)

Model checking tools

• CADP - Construction and Analysis of Distributed Processes
• CBMC - a bounded model checker for C/C++ programs
• DiVinE - Distributed Verification Environment
• EmbeddedValidator, The Matlab/Simulink/Stateflow/Targetlink Formal Verification Environment
• FHP-Murphi - Finite Horizon Probabilistic Murphi
• GEAR, a game based model checking tool capable of CTL, modal µ-calculus and specification patterns.
• Helena — High Level Colored Petri Nets Analyzer
• LASH, Liège Automata-based Symbolic Handler
• LTSA, Labelled Transition System Analyser -- Imperial College, London
• [mc]square, a model checker for microcontroller (ATMEL ATmega and Infineon XC167) assembly code
• MOPED
• MOPS, Modelchecking Programs for Security properties
• CMurphi Caching Murphi
• μCRL, GPL, Based on ACP
• mCRL2 Toolset, Boost Software License, Based on ACP
• ORIS, uses a CTL-like temporal logic with real-time bounds, action and state based.
• ProB
• PRrobabilistIc Symbolic Model checker (PRISM)
• ProofPower
• PROSPER - a formal design tool that incorporates model checking
• Prover Plug-In commercial proof engines
• RAVEN (Real-Time Analysis and Verification Environment)
• RuleBase
• SLAM and Static Driver Verifier (SDV) - CEGAR-style model checking for systems code
• Symbolic Model Checker (SMV), the original symbolic model checker
• Statemate ModelChecker, Statemate Models Robustness Checking
• Statemate ModelCertifier, Statemate Models Requirements Certification
• Statestep Specification and modeling tool; checks that invalid states are not reachable.
• StEAM (State Exploring Assemblylevel Model Checker) Verification of concurrent C++ programs
• TEMPO Modeling and verification environment for realtime and hybrid systems
• TLC
• Temporal Logic Verifier (TLV)
• Terminator Verification of termination and other liveness properties for the C programming language
• Uppaal Model Checker (UPPAAL)
• Model checker for Verilog based on CEGAR (VCEGAR)
• Verification Interacting with Synthesis (VIS)

Other

• Database of Verification and Model Checking Tools (Yahoda)

Research groups

• Formal-V group — Indian Institute Of Technology, Kharagpur, India
• UCLID group at UC Berkeley
• Software Design Group at MIT
• Automated Reasoning Systems (SRA) - at Bruno Kessler Foundation, Trento Italy
• Modelling and Analysis of Complex Systems group at The University of Birmingham, England
• Software Modeling and Verification (MOVES) group at RWTH Aachen University, Germany
• Formal Methods & Tools (FMT) group at The University of Twente, The Netherlands
• Model Checking at Carnegie Mellon University
• Software Verification and Validation at UT Austin
• SAnToS Laboratory at K-State
• Automated Software Engineering at Nasa Ames Research Center
• NASA/JPL Laboratory for Reliable Software
• VLSI/CAD Research group — University of Colorado at Boulder
• Formal Methods Research Group, University of Utah
• Verification and Validation — Brigham Young University, Provo, Utah
• ParaDiSe Laboratory — Masaryk University in Brno
• VASY Research team — INRIA Rhône-Alpes, France
• Software Modeling and Verification (SMV) group — University of Geneva (Switzerland)

Why link yet another two mc tools

I removed the following links:

tools

• Charmy, CHARMY: A Framework for Designing and Verifying Architectural Specifications

External link

• 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.

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. — Bilorv (talk) 22:52, 15 July 2020 (UTC)

Agree - 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. — Bilorv (talk) 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: Springer web page. --JonathenHarker (talk) 12:26, 13 December 2020 (UTC)

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