Augmenting synchronous and asynchronous monitors in ELARVA

Abstract

Runtime verification has steadily been gaining more popularity, but skepticism still exists regarding its applicability in systems. Runtime verification techniques are increasingly being applied in industry as a lightweight formal approach to achieve added assurance of correctness at runtime. A monitor is typically introduced in order to verify system, according to some properties defined. In asynchronous monitoring, when an event occurs, the target system notifies the monitor with the occurrence of such an event. Execution on the target system is allowed to continue, irrespective of whether the monitor has verified such event or not. In this scenario, the target system and the monitoring process could be running either on a separate processor or on the same processor. In the former scenario, execution of the target system is uninterrupted since both processes are running in parallel on different processors, while in the latter, the scheduler must context switch between processes. Although such approach minimizes the overheads created, violations could be detected late. Furthermore, in synchronous monitoring, the target system is required to pause execution once an event occurs, until the monitor verifies such event. Once such verification completes, the target system is allowed to continue. This ensures that when a violation is detected, the target system never continues to execute, eliminating further damages from occurring. On the other hand, the overheads created might slow down the system drastically. Executing the target system and the monitoring process on the same processor or on two distinct processors shall not gain any performance, due to the fact that the target system shall be idle while verifying. ELARVA is a runtime verification tool, used to ensure correctness of systems written in Erlang, at runtime. Currently, ELARVA is capable of monitoring a system in an asynchronous fashion, with the possibility of events being detected late. Therefore, the aim of this FYP is to investigate how synchronous and asynchronous monitoring could be augmented. Such concepts could then be applied on ELARVA in order to allow the possibility of switching between synchronous and asynchronous monitoring at runtime. In order to augment both types of monitors in ELARVA, the use of aspect oriented programming was used, where the injected code at designated pointcuts shall notify the required monitor with the occurrence of such event. In order to evaluate my findings, I have opted to monitor a system in three ways by using; a synchronous monitor, an asynchronous monitor and a combination of both by switching between monitors appropriately at runtime. In the latter, critical events were monitored synchronously, while non-critical events were monitored asynchronously. When monitoring synchronously and asynchronously, the overheads complement to 39% and 163 respectively. On the other hand, when the system was monitored by switching between monitors accordingly, the 'Overheads created were of approximately 193. Although such figure is slightly higher than asynchronous monitoring, it ensures that critical events were verified on time.