Is there a simple Model Checker tool. I am planning to implement a model checker tool which will analyze the code for some of the predefined properties.
A:
CBMC is one simple-ish tool I'm aware of that actually operates on code. Model checking in general is a heavily-researched field, but as folks have already commented, this breadth makes it difficult to suggest something with the info provided. There are thousands of SAT solvers, formal tools for HDL/state machine verification, and plenty of commercial static source analyzers.
In any case, CBMC is a good tool, but don't take my word for it; Ed Clarke, the main faculty member behind this work, won the Turing Award this year ;-)
Matt J
2008-10-20 16:17:03
A Model checker tool which maintains states. i.e., I am planning to implement a Tool which can say whether the application terminates or not. (Only static analysis)
Vinay
2008-10-20 16:19:28
Really? That seems a bit difficult (http://en.wikipedia.org/wiki/Halting_problem) ;-)
Matt J
2009-03-01 19:26:41
+4
A:
One important tool is SPIN, with the Promela language. If you use LaTeX, there is also TLA+.
These will not analyse your code, but will let you express a model for your assumtions and state transitons, and will then analyse for invalid states. In other words, they will detect problems in your model, not the implementation of your model.
I have seen a demo of Goanna, but I don't know if it is available at all (commercial or otherwise); this has the advantage of actually analysing your source code.
Just looking at your question, and the comments in your question again, it sounds like you really should read some of the literature first. Perhaps, The Spin Model Checker, or Specifying Systems (downloadable from Leslie Lamport's website). You need to reframe your problem so that you don't try to solve the halting problem.
janm
2008-10-21 10:34:49