Counter example visualization for runtime verification

Abstract

Most functionality in an application is tested by exhausting most of the possibilities one could do in it until either it is statistically robust or a bug emerges. While testing accommodates most of the applications developed, it is not enough for more complex and critical systems since it is an ad-hoe approach and thus testing manages to expose only a subset of bugs inside a system. Model checking can be used to overcome this drawback by' formally checking whether a system conforms to a given set of requirements, such as ensuring that the system does not enter a known bad state. Unfortunately, model checking is not ideal since it must exhaust all of the execution paths of a system to ensure that all of them do not violate the given specifications. Runtime verification is another alternative to model checking, which although very similar, the former only monitors the current execution path of a running system and detects whenever a specification has been violated. Specifications are defined in some mathematical language and thus if a specification is written in some other language it must be reduced to the native language of the runtime verification tool to work. "While this is plausible (since the specifications can be supported by the runtime verification tool by creating automatic converters), it lacks correspondence between the initial language and the new converted language. This issue is encountered whenever the runtime verification tool represents where the violation has occurred in the specification. Since it has been converted to the native language, and the specification writer might not comprehend it, the indication to where the violation has occurred is rendered useless. In this report we will look at the Larva Interpretation Framework which provides two approaches to help interpret the representation back to the original language for the user to understand. Furthermore, this report will also propose an extra solution to enrich the representation of the specification, by allowing the user to visualize the specification on screen for better comprehension. Usually, users are expected to report whenever a bug occurs in the system, by supplying a user story which is usually a narrative description of what the user did during system usage, such as the click of buttons, keyboard presses and other similar factors. This however is very subjective due to the natural way of telling them and thus it is not very ideal. Instead, recording and replay systems are used to consistently record system activity during runtime, which can be replayed at a later stage. These propose a formal way of describing a system activity during runtime, with the ability to replay the record and thus make the bug occur once again and thus is an excellent tool for the developer to quickly identify the root of the bug. Unfortunately, all of these systems are found at low-level and thus introduces restriction of portability to an application. Several recording systems exist for Java applications, however there are implemented in the JVM or Java API and therefore suffer from low-level restrictions. This dissertation will propose HiRec, a new recording system which is planted at a higher level without modifying any of the JVM/Java API, retaining all of the portability while still being able to record and re-orchestrate the execution path of that record.