|
Debugging the tip of the iceberg Darko Marinov
Professor Darko Marinov wants you to be able to trust that your program is correct and reliable. Programs usually fall into two categories: those that manipulate complex data and those that are control intensive. Marinov's goal is get rid of as many bugs as he can in data intensive programs by creating software testing tools. Some designers and users are willing to accept bugs. Not Marinov. "I'm always trying to find more bugs and eliminate them." Marinov's recent work was an extention of his PhD thesis research, during which he wrote a tool for automatic generation of test inputs for programs that manipulate complex data. He applied the tool in system testing (which tests an entire program) and in unit testing (which divides a program into small units that can be tested in isolation). According to Marinov, unit testing is very important. "The basic blocks need to be correct if you're going to build a whole system," he said. "If the bricks are falling apart, it's hard to build an entire house from them. By testing smaller units, you can do more exhaustive testing without worrying about scaling. You can torture the code more." So how do you come up with the appropriate test inputs for a program unit? Think of all possible test inputs as an iceberg. It would be impractical to test all the inputs in that iceberg. One thing you can do is random testing across the entire iceberg. But if it's a large iceberg, it's not much of an improvement. Marinov's unit testing looks at just the tip of the iceberg and performs bounded exhaustive testing within that chunk. Suppose you are testing a program that manipulates web pages. You can test it with a small number of large web pages or with a large number of small web pages. Marinov's method will choose the large number of small web pages because by exhaustively testing this set, many bugs will turn up. Another way to generate inputs in unit testing is to use symbolic execution. Consider, for example, a swap function that changes the values of x and y by a sequence of assignment (x=x+y, y=x-y, x=x-y). You can test this piece of code by plugging in different values for x and y and seeing if you get the correct answer. But you can't plug in all values for x and y. It would take forever. Using bounded exhaustive testing, you can plug, say, all values less than a certain amount and keep testing until you've reached the top value. Instead of using different sets of values to prove that the swap function works, you can use symbolic values that hold true for all possible values. In other words, instead of plugging in 5 for x and 3 for y, you plug in unknowns like ? and ?. In this way, you can prove whether the function works for all possible values of ? and ?. The underlying technology for the simplification behind symbolic execution is based on theorem provers. Automatic theorem provers (those that do not require human intervention) have theoretical limits, however. There are things they can decide and things they can't. If a program contains undecidables, it cannot be fully tested using symbolic execution. In the previous example, assignments used only addition and subtraction to accomplish the swap. But if you do something that involves, say, multiplication, symbolic execution may fall apart as the expressions become complex and undecidable in general. You can then go back to either bounded exhaustive testing or even random testing. Written by Judy Tolliver, July 17, 2006
|
|