Most of this article may seem like I am stating the obvious (offcourse unlike the rest of my blog!). I have been attending a course on Programming Languages by Prof Wesley Weimer. Been quite awesome till date. We were speaking about static analysis of programming languages and the success of Microsoft’s SLAM project in automatically finding bugs in Windows Device Drivers by testing their compliance to the Operating System’s API specifications.
This blog is about model checking or checking every state of a finite state automata system just so as to make sure that some undesirable states are unreachable in real time. To make this sound more human, you want to exhaustively test a system by bringing it to all possible scenarios(states) that it can encounter during the course of its life and ensuring that none of these scenarios get it to misbehave. Quite like any normal tester would want to do.
However the need to formalize the concept comes in only because of the practical difficulties involved in bringing every system to all states and testing it exhaustively. This is particularly applicable to software and prog languages. For example, if you are writing your program in a language that supports complex types i.e most object oriented languages, you are basically in an infinite state space. Even simpler languages that have not support for OO techniques are difficult to exhaustively test. If your language supports long numbers for example, every possible that a particular long variable might assume might introduce a new state in the program. Technically your program could show behavioral difference only selectively i.e if long_var>1000 perform_action1 else perform_action2. However, there are still infinite state spaces in the above case if (say) comparison in long variables is not an atomic action in the language that you are programming. Concurrency will bring in infinite state spaces #fail
In the past week I have come across so many papers and tools that do exactly the same thing and call it different things. SLAM from Microsoft is the original (I think). All these software and code testing tools bring in some sort of abstraction or modelling into the system and then exhaustively test the space that can be occupied by the code. Clearly, the abstraction reduces the states that can be occupied. In the case of SLAM this abstraction seems to be by reducing C programming Language’s type system to only a boolean type system, clearly removing the infiniteness of the space caused by complex types. Quite ingenious.
Whats been striking is the number of other tools that seem to be doing things that are similar. I do not want to trash any of these on a public post, but this one in particular was just unavoidable.
State explosion of software systems is just a complex way of saying that it is not possible to exhaustively test software. Knuth’s famous “I have not tested these algorithms but only proved them to be correct” yada, yada are causally related to this. Inspite of model checking mostly stating the obvious, I loved the math. Quite analogous to a reason I like programming. Not too many people seem to get it.