Markov chains and formal proofs

I’ve posted this link before, when this blog was on the late lamented Posterous, but when I went looking for it again, it had disappeared - so here it is again, for good measure. Hat tip to Kent Beck for originally tweeting about this article explaining Markov chains.

I’m reading some interesting follow-on papers, in particular, a pair by James A Whittaker (Yes, that James A Whittaker) A Markov Chain Model for Statistical Software Testing and Markov Analysis of Software Specifications as well as a graduate thesis by Ivan S. Zapreev entitled Model Checking Markov Chains: Techniques and Tools. I’m interested in the effect of a program’s cyclomatic complexity on the feasibility of using Markov chains for testing purposes.

Until now, I haven’t found formal proofs of anything other than trivial software systems to be convincing; they appear to rely on a perfect test oracle, namely a specification that’s so well specified that it may as well be the software system itself. Formal approaches such as Dijkstra’s tend to approach software systems in some idealised way, not as gloriously nonlinear entities executing on top of preemptively multi-tasking operating systems and making use of imperfect APIs over unreliable networks… and even if I concede that it’s possible to prove that a software system is internally perfectly consistent, that tells me nothing about how well that system actually solves the needs of the customer paying for it.

But in any case, I think Markov chains are worth exploring.

May 8, 2013

Previous post
Stop using spreadsheets If you use spreadsheet software, but you don’t use any mathematical functions, please stop right now. You’re inflicting pain on yourself and your
Next post
“Simply hold the ctrl key and double click on any non-button area of the window chrome - not the contents” I work with software, a lot. It’s probably safe to say I live software. So I’m comfortable with the idioms of software development and software