Group colloquium: Combined Static and Runtime Verification of Distributed Objects

During my research visit to Chalmers university in Gothenburg, Sweden, I worked on runtime verification of distributed Java programs in the context of the StaRVOOrS project. We target distributed Java programs written in the ProActive programming platform, which implements the "Active Objects" design pattern. In essence, ProActive allows to register Java objects as being 'active', thereby enabling other JVM instances to call the public methods of these objects, even by JVM instances that are located on different machines. Runtime verification is performed by assigning to each participating JVM instance a runtime monitor, which describes its allowed behaviour. To keep this setup compositional and efficient, we use assumption-commitment reasoning, so that the runtime monitors can efficiently distinguish between violations from the environment and (local) violations from the Java implementation that is being monitored.

In this informal talk I will give an overview of our verification approach and demonstrate this. I will also discuss how our approach can be combined with static verification.