Statistics and runtime verification

Abstract

Software is influencing our lives in more frequent and crucial ways. This implies an ever increasing need for reliable software, whereby such reliability can be guaranteed through a method which guarantees software correctness i.e. that the system implementation adheres to its corresponding specification. This field is commonly known as software verification, and admits multiple techniques such as testing and model checking. However, given the intractability of verifying each execution trace, and the lack of coverage implied by testing we require a new approach to the field. This is provided by runtime verification, whose concern is the verification of the currently executing system trace, and can be considered as an extension to testing with augmented guarantees through the use of more powerful specification languages. We theorise that augmenting runtime verification with statistics is advantageous. Firstly, it is often better to watch for indicators of failure than to wait for failure. Also, statistics allow for the straightforward specification of non-functional requirements, such as specifications related to performance and reliability (as opposed to most runtime verification logics which solely focus on functional requirement specification). Moreover, from a utilitarian point of view the collection of statistics over runtime executions allows for applications to fields such as performance profiling, intrusion detection, user modelling and quality of service. Finally, augmenting a logic used for runtime verification with statistical capabilities may increase the logic expressivity, or at least increases the conciseness and intuitive expression of certain system specifications. The augmentation of runtime verification with the notion of statistics implies the need for an underlying runtime verification framework. We identify this framework to be LARVA, an event-based runtime verification tool for monitoring temporal and contextual properties of Java programs. Based on Dynamic Automata with Timers and Events (DATEs) as the underlying mathematical framework, LARVA allows for the expression of (i) Temporal aspects dealing with consequentiality and real time (ii) contextual aspects with the possibility of monitoring objects either globally, grouped according to their context or individually (iii) Exceptional program executions. This thesis is primarily concerned with the extension of the LARVA tool and logic with statistical capabilities. This is achieved through the creation of a statistical framework operating on top of the current logic, with the result being a runtime verification tool capable of expressing statistics, henceforth called LarvaStat. The creation of LarvaStat involves a number of steps, the first being the conceptualisation of the core notions driving the statistical framework. Following this, we also present a formal analysis of the resulting framework through the specification of a formal semantics expressing the statistical logic. With the theory complete, we present a domain specific embedded language extending LARVA, thus offering a medium for the expression of statistics. The final step involves the implementation of a compiler, which converts statistics expressed using the defined language into an executable artefact. Finally, we also present a comprehensive case study for the justification of LarvaStat based on Intrusion Detection.