Modeling Stochastic Systems in Spec Explorer

One of the more advanced – and powerful – features of Spec Explorer is its ability to handle stochastic SUTs. Stochasticity is common in systems with external dependencies, this could for example be the file system, network interface or external devices. Common for all these dependencies is that they sometimes fail for various reasons. You cannot predict when this will happen, and for the most part in Software testing we strive to avoid these spurious behaviors at all cost.

Another source of stochasticity is the use of random in the SUT (which I will explore a bit more in this post) or stochastic behavior due to race-conditions in multi-threaded applications (which I will investigate further in a later post).

First of all, what does a stochastic model look like? Take a look here:

This picture represents a model of a stochastic accumulator. It shows a slice where the accumulator is increased twice then reset. Each addition is stochastic in that it can add either 1 or 2 to the counter.

When working with stochastic models, in addition to the normal “round” states, Spec Explorer introduces diamond-shaped decision states. Each diamond represents a choice in the model where the SUT can behave in one of many ways. In the case of the stochastic accumulator we can see that the value of the accumulator can go from the initial value of 0 to either 1 or 2 in the first addition step.