Combining Monitoring with Run-time Assertion Checking

Stijn de Gouw

Promotor: prof.dr. F.S. de Boer (CWI and UL)
Co-promotor: dr. M.M. Bonsangue (UL)
Universiteit Leiden
Date: 18 December, 2013, 10:00


According to a recent study by Cambridge University, software bugs anually cost 312 billion dollar globally. Type Checking, Static Verification and Run-time Checking are well-known methods to prevent bugs, isolate bugs and software. All three methods determine whether the software works as intended by means of annotations: a formal description of the desired behavior of the software.

In this dissertation we developed a new technique for Run-time Checking for two object-oriented languages: Java and the Abstract Behavioral Specification language ABS. The ABS is a language developed in the European HATS project that supports concurrency by means of concurrently running groups of objects. In object-oriented languages, objects communicate by sending each other messages. The behavior of objects is completely determined by the order in which the messages are sent, and their content. Traditional methods for Run-time Checking focus either exclusively on the description and testing of the order of the messages (Monitoring), or they focus on specifying and testing the content of those messages (Run-time Assertion Checking, Design by Contract). The technique introduced in this dissertation combines Monitoring with Run-time Assertion Checking.

The basic idea behind our technique is that the behavior of objects can be described formally by means of an attribute grammar extended with assertions. The underlying (context-free) grammar specifies the valid orderings of the messages in a declarative manner, the attributes define properties of the contents of the messages, and assertions specify the desired values of those properties. If the assertions are quantifier-free, it is decidable whether an execution of a program satisfies a specification as given by such an attribute grammar. We have developed a new Run-time Checker for attribute grammars in the form of a meta-program in the language Rascal. We applied the Run-time Checker to an industrial case of the e-commerce company Fredhopper. On the basis of this case study we investigated the efficiency of the run-time checker, and successfully discovered and solved several bugs in the Fredhopper software.