Generating test cases through ModelJUnit for LARVA specifications

Abstract

The issue of software correctness is a central issue in software development and this can be tackled through various methods. The aim of such methods is that of checking whether a particular system respects the initial set of specifications. Testing is the technique that is most commonly used for such process, but alternative approaches, like runtime verification, are becoming more popular within the area of Formal Methods. The main distinction between testing and runtime verification is that testing attempts to check a number of representative system behaviours while runtime verification aims at checking one particular system behaviour: the one observed at runtime. Considering this close relationship between testing and runtime verification, the main motivation of this project is to combine both techniques into one tool, which would make it possible for test cases to be automatically generated from runtime verification specifications. In this report, I provide a background on Runtime Verification and Testing, in particular, two tools that will be used in this project, namely LARVA and ModelJUnit. These tools will be combined together to help reaching the aim of using runtime verification specifications to automatically generate test cases. The main hurdle of automated test case generation is to generate tests which cover relevant system behaviour to maximise the probability of detecting bugs. While automated test case generation can be done using a completely random approach, the objective of this project is to exploit runtime verification specifications to improve the quality of the test cases. Essentially, this should enable us to cover more system state space using fewer tests than a random approach. The project takes a LARVA script with system properties, as an input, and generates a model which is compatible with ModelJUnit. Such a model acts as a guide for the automatic test case generation, avoiding steps which do not contribute to more state space exploration. After testing and evaluating the model classes against a typical Java system, it was noted that the generated tests covered the system state space in less steps when compared to a generic model that doesn't include monitoring.