An Eclipse plug-in for polyLARVA

Abstract

Runtime verification is a software verification technique involving a monitoring agent which monitors a system at runtime. The polyLARVA tool implements this verification technique and is designed to be agnostic to the language of the system being monitored and to enable the monitoring of multiple systems. Its use in commercial software development is however limited by the lack of integration of the tool with development environments. Integrated development environments (IDEs) are collections of tools which are designed to help developers in their tasks, presented in an integrated interface. The proposed solution for this is the integration of polyLARVA with the Eclipse IDE, through the development of a plug-in. A benefit of this is that the verification process will be integrated within software development. The polyLARVA tool itself will also benefit from the advantages of using an IDE: automation of simple repetitive tasks, a centralised environment for all steps in the development cycle and other tools which increase the productivity of developers. The design of the plug-in is derived from a study of the different actions involved when using the polyLARVA tool. These include writing the specification script, compiling and running the monitor (and the system with monitoring enabled) and finally debugging the system and the monitor together. Each is addressed by developing features and by using existing tools where possible. The plug-in is also designed to be extendible to new system languages. This extendibility includes language-specific editing features and system launching. The plug-in is then evaluated by testing it in different scenarios and by observing test subjects using the plug-in. The overall results are that while most aspects and functional and do provide advantages over using polyLARVA without the plugin, there is room for improvement, through the development of more features and refinement of existing ones.