Talk:Model checking

From Wikipedia, the free encyclopedia

This article was originally based on material from the Free On-line Dictionary of Computing, which is licensed under the GFDL.

This is the talk page for discussing improvements to the Model checking article.
Article policies

I edit see also.. Taehoon

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

Contents

[edit] 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).

[edit] 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)

[edit] 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)

[edit] 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)