Extraction of Probabilistic Behaviour Models based on Contexts

Model extraction allows the automatic construction of behaviour models from an available implementation, which can be fed into existing analysis tools. Even though these models are usually analysed using qualitative properties, many interesting and relevant properties of current systems are related to quantitative aspects, such as the probability of reaching a certain state or how many times a certain task is expected to be executed. In this work, we extend an existing model extraction approach to include probabilistic information. The original approach creates Labelled Transition Systems (LTS) from Java code based on execution traces. The traces are processed by a tool that identifies contexts, which represent abstract states of the system, considering static and dynamic information, producing context traces. We use these context traces to calculate transition probabilities and generate models in the input language of a probabilistic model checker. We evaluate our approach in case studies and demonstrate that, by using context traces rather than simple traces, we produce more accurate models, thereby with probabilistic information closer to the real behaviour of programs, based on their observed traces. We also show how to build models of programs with single and multiple components.