Practical runtime monitoring with impact guarantees of Java programs with real-time constraints

Abstract

With the ever growing need of robust and reliable software, formal methods are increasingly being employed. A recurrent problem is the intractability of exhaustively verifying software. Due to its scalability to real-life systems, testing has been used extensively to verify software. However, testing usually lacks coverage. Runtime verification is a compromise whereby the current execution trace is verified during runtime. Thus, it scales well without loss of coverage. In this thesis, we examine closely the work in runtime verification and identify potential improvements with regards to the specification of properties and guarantees which are given. For the first issue of specification we make use of a real-life case study to better understand the day-to-day properties which system architects would need to formalise. DATE is the logic which results from these experiments and experiences. It is shown to be highly expressive and versatile for real-life scenarios. This is further confirmed by the second case study carried out and presented in this work. Our logic requires a complete architecture to be usable with Java programs. This architecture, called LARVA, is developed using Java and Aspect J with the aim of being able to automatically create and instrument monitoring code from a LARVA script. A central aspect of this thesis is the work on real-time properties. Such properties are very sensitive to overheads, because overheads slow down the system and use up resources. For this purpose, we present a theory based on the prominent real-time logic, duration calculus, to be able to give guarantees on the effects of slowing down/speeding up the target system clue to the monitoring overhead. Another form of guarantee which we can give on real-time properties is the upperbound of memory overhead used during runtime verification. This is achieved by starting from the subset of duration calculus, QDDC, and translating it into Lustre. To relate LARVA to other tools in the field we use a benchmark to compare expressivity and resource consumption of LARVA to other prominent tools. Furthermore, a subset of duration calculus (counterexample traces), QDDC, and Lustre have been shown to be translatable into LARVA. This has two main purposes: first that this allows users familiar with other logics to utilise LARVA, and second that the guarantees enjoyed by these logics, will also benefit LARVA.