Feat/markov chain

[stevana]

Things left to do, probably in separate PRs:

• Refactor the StateMachine record to contain either a simple generator, model Symbolic -> Gen (cmd Symbolic) or the Markov chain approach (this would be a breaking change);
• ~Update changelog~;
• Analyse Markov chains for termination; it should be possible to reach all states and eventually end up in a terminating state.

[fenollp]

Hi there, I’m trying to understand what this brings and am not familiar with the Cleanroom literature. Can you provide me with a link to some expression of this: usage, how it works, ... Thanks! I am mostly familiar with the Erlang side of QuickCheck and some papers such as https://scholarworks.iupui.edu/handle/1805/15838 This sounds interesting but I am not sure I am understanding much.

[stevana]

Sure, the basic idea is to describe generation of programs as Markov chains. To do this we need a finite set of states, and for each state we have a set of generators that with some probability generate an action and transition into the next state (if the set of generators is empty we stop generating). Since these states need to be finite, they can't in general be the same as our model, which often is infinite. I believe that in the Proper Erlang library there's a similar distinction between state (finite) and state_data (possibly infinite)?

The benefit is that Markov chains have been studied in math and other fields, and there are many interesting analysis that you can perform on them (even before we use them to generate programs). For example, from the Markov chain we can calculate:

• Average program (sequence of actions) length
• What fraction of time one typically spends in one particular state (node in the chain) or action (arc in the chain)
• Average number of test cases we need to generate before we end up in some state
• Average number of test cases we need to generate to cover all states/actions

But it get even more interesting once we generated and tested the programs. If we record what the number of successful and unsuccessful times we went from one state to another, then we can calculate an overall reliability of the system. For example, we will be able to say things like: statistically, if you generate a random program with the Markov chain, then with 95% confidence that program will behave according to the specification in 83% of the time.

We've started a separate library for the Markov chain calculations here. The README contains links to a couple of calculation heavy papers, but unfortunately there's not really a good up to date reference that I can link you to. The problem is that the research here started as part of the Cleanroom method in the 80-90s, they published a couple of books on the topic, but then the research moved on, some of the original authors have since passed away and nobody has kept an up to date reference as far as I know.

If you are really interested, I'd recommend reading some of the early papers, e.g.:

• J. A. Whittaker and J. H. Poore. Markov analysis of software specifications. ACM Transactions on Software Engineering and Methodology, 2(1):93–106, 1993
• J. A. Whittaker and M. G. Thomason. A Markov chain model for statistical software testing. IEEE Transactions on Software Engineering, 30(10):812–824, 1994
• G. H. Walton, J. H. Poore, and C. J. Trammell. Statistical testing of software based on a usage model. Software Practice & Experience, 25(1):97–108, 1995

These will give you a basic picture of the original idea, but keep in mind that things have moved on since (don't read into the details too much). For a recent (2017) case study, see:

• Improving test adequacy and software reliability with practices of statistical testing by Yufeng Xue, Lan Lin, et al.

This should give you a more up to date picture (even though I must confess that the example they use still doesn't make sense to me and I've tried to understand it several times). That paper contains the statistical analysis made by their tool JUMBL (written in Java). For details on how exactly those calculations are made, see:

• Computations for Markov Chain Usage Models (2000) by S. J. Prowell

That last report is available online for free, but the papers you'll probably need to use Sci-hub for.

If you have any further questions, feel free to ask!