Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2012-01-23 04:41:49
- awesan
- Member
- Registered: 2011-04-30
- Posts: 45
Static/Dynamic analysis tools vs model checking tools
I see a list of static analysis tools at http://spinroot.com/static/. I have used the old generation of tools such as lint. But looking at the description/white-papers on the newer generation of tools such as CodeSonar and Coverity, it looks like they seem to do whole program analysis that finds errors such as deadlocks. They also seem to allow annotations to check temporal properties per their white-papers and allow calling into the IR (Intermediate Representation) to check more user-defined properties in the whole program analysis. Though I have not personally used these tools, if they work like a charm (I guess users may have to do with false positives to some/great extent), then it would alleviate some burden of using model checkers such as SPIN and UPPAAL. With model checkers, though learning the model checker and using it is one aspect, accurate mapping of the model to the actual program in languages such as C++, Java could be tricky and challenging and a bigger challenge would be to maintain the model as the actual program changes through different releases and patches. So, I am wondering what the gaps/advantages are in using the tools such as CodeSonar and the model checkers? What are the advantages of the model checkers that even the new generation of code analysis tools have not achieved (and they cannot possibly achieve or very hard to achieve)?
Offline
#2 2012-01-23 05:41:08
Re: Static/Dynamic analysis tools vs model checking tools
It is definitely true that static analyzers are easier to use than model checkers.
And they are valuablue, because they can quickly catch common coding mistakes and identify known vulnerabilities in code.
But they cannot do analysis of the type that logic model checkers can do. The investment (in time and effort) in using a model checker is much greater, but the potential payoff is also greater.
Clearly though, the leading static analyzers are very very good and are used much more widely than model checkers.
Offline