4

Has anyone have contact with model checking with this tool SPIN, even more any information of model checking (concurrent programs)

edgarmtze
  • 24,683
  • 80
  • 235
  • 386

1 Answers1

6

Yes, SPIN is a very good model checker but I am wondering what you want? Do you just want to hear that yes, I have heard and played with SPIN or do you want suggestions for how to model check source code?

For example, if you're a C programmer, get your hands in ESBMC, write a little program and run ESBMC on it.

That should get you started to understanding what can be done and how to do it. By the way, for starters Model Checking is not static analysis. It is actually much more powerful. It's the anti-static analysis. Model Checking actually 'in a (very narrow) sense' simulates your program and find situations (argument combinations, exceptional situations, border cases) where it would actually fail.

Paulo Matos
  • 1,614
  • 17
  • 23
  • 2
    Eh? It is *exactly* static analysis: it reasons from the source code. You might argue it is different than other static analyzers, but I don't see what point that serves; they're all different. – Ira Baxter Jul 20 '11 at 16:42
  • Sorry, it is not. The code is analysed dynamically, therefore it is not static. Model checkers don't execute the code 'per se' but generate models which are simulated. Therefore it is not static analysis. lint is a static analyser. SPIN is not. – Paulo Matos Jul 28 '11 at 08:23
  • 4
    I think your definitions are confused. Dynamic analysis means to capture information as the *program* runs. With SPIN, you extract a abstract model of the program (generally using static analysis!) and then SPIN enumerates the state space. Simulation of the state space is not anything close to program exeuction. There is no "program" to execute at this point. – Ira Baxter Jul 28 '11 at 11:37
  • 1
    SPIN is NOT a static analyzer. For anyone still in doubt, refer to: [C Static Analyzers Overview](http://spinroot.com/static/), [Static Program Analysis](http://en.wikipedia.org/wiki/Static_code_analysis), [Dynamic Program Analysis](http://en.wikipedia.org/wiki/Dynamic_program_analysis). Also, note that extraction of a Promela model from C sources is far from a trivial or widely automated procedure, and is certainly itself a completely different thing from static analysis. Also, simulation of the state space IS program execution. Due to state space explosion, usually we use partial simulation. – 0 _ Jul 26 '13 at 00:43