State-based monitoring using LARVA

Abstract

With the increasing size and complexity of computer systems, the need for verification of software is becoming more and more important. Software verification may be done using several techniques such as testing and model checking. Unfortunately, testing cannot always guarantee that the system is free from bugs and model checking does not scale up well with the size of the system. Therefore, runtime verification was developed with the aim of allowing a system to be verified while it is running by monitoring the activities occurring within the system and checking them against properties describing its expected behaviour. However, runtime verification is limited by the events which can be monitored as they are usually based on particular points of interest in the program's control structure such as method calls and exception throws. Therefore, one might not be able to monitor specific points of interest based on the changes in the state of the system. This refers to monitoring changes in the system's data such as the value of variables. Even so, checking the system's state every time it may have changed could lead to an increase in the resource overhead. Thus, in this project, we address these problems by presenting a solution which can monitor the state of a system without extensive resource overhead by extending the functionality provided by the runtime verification tool LARVA. Our solution gives the user the ability to express properties on the field variables of their system in order to capture changes in their values. We also allow the user to specify particular types of events such as when a value falls below, or changes to, a specific value. We applied our solution to several case studies in order to assess and evaluate the usefulness and feasibility of the provided state-based monitoring and show how it can be beneficial to real-life systems.