Saturday, August 21, 2004

Static Analysis tools for the uninitiated - 2

Amit: Yes it should be similar to PC-Lint. I haven't used/evaluated any of these two but they are both good examples.

Static analysis tools can understand rules which can be added by the user provided they fall into certain types. More formally they should be some kind of logic formulae. e.g If method X() is called, method Y() should be called at least once after method X() has been called. This would probably (I am bad at logic and maths :)) be a rule that can be expressed in temporal logic. The analysis tool takes in such rules, checks your code for violations of these rules and then reports these as bugs.

Model checking is another technique used for verification. Microsoft uses a tool called SLAM for device driver verification. Protocol designers also use model checking. In model checking the user has to provide an abstract model of the program against which the program is verified. Generally this can take a lot of "ramping up time" if you need to specify the model since it writing a model means that a person has full understanding of the program.

Regarding the comments: I have ditched the haloscan comments now and use blogger comments, but anonymous comments are allowed. In the sign-in page you have a link which allows you to post comments anonymously.

1 comment:

Anonymous said...

OK, got it.I have used PC Lint and it is different... When u say that this particular tool will check if func X() is called before func Y(), then I guess that it takes some form of 'sequence diagram' as a 'rule' to validate the code..and if that is true then this ought to be a awesome tool but it requires deep insight on part of the rule writer, into the code which needs to be verified. So to summarize, such tools are very useful in theory, but practically most of the time s/w design is so much flawed and hap hazard, that rule writing becomes next to impossible...& then u end up 'masking' some of the rules and finding work arounds in the tool being used for static code analysis...we do that regularly in PC lint...and that beats the basic purpose...I therefore believe that instead of working on such "static design verification tools" companies should focus more on developing intelliegnt s/w design tools itself and try to make as them fool proof as possible..
~Amit