Skip navigation

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.


One Comment

  1. interesting read.. but this level of abstraction can be possible for people who develop system level code and one who knows a lot about operating systems.. Awaiting more posts regarding this 🙂

One Trackback/Pingback

  1. […] State Space Explosion is what limits checker from being built at run time. So what do you do? Build some abstractions over some things in your program and keep asserting these at all points. For eg: My mutex C program should never call unlock or lock twice continuously– clearly a cause for deadlock. This is a predicate that is invariant over the lifetime of a program (Did I just say lifetime? Rich Hickey influence I guess). Now, how does one make these abstractions? Remove all lines of code in your program that are not associated to the assertion(s) you are making and retain just those that are. […]

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: