Expressing runtime verification properties using regular expression in LARVA

Abstract

Due to the ubiquity of software systems, software verification becomes increasingly more invaluable. There are multiple techniques for verifying software such as model checking and testing, however, these techniques are inadequate for large-scale systems and cannot fully guarantee the correctness of the system, respectively. Therefore, runtime verification was proposed and developed as it verifies the system whilst the system is running by checking against the properties expressed by the user. In this project, a runtime verification tool called LARVA, is used where the user expresses the target system's properties in its own language called Dynamic Automata Timers and Events, in short DATEs. However, this language is not well-known in the computing field. Therefore, we address this problem by proposing that the properties are expressed by a more widely known formalism, regular expressions. Our solution would extend the LARVA tool and solve the issues in expressing properties by using a more established formalism and making the LARVA tool more practical. It is crucial to ensure overheads are kept low and that we explore two approaches in translating regular expression into DATEs. These two approaches are using the regular expressions' derivatives, as well as, transforming the regular expressions into a deterministic finite automaton. In order to observe which approach is the most efficient in terms of memory induced and computation time when verifying the system, we apply our solution to a case study to evaluate the cost of monitoring that system. We conclude that the derivative approach is the more efficient approach both time-wise and memory induced.