Publications about Jassda

Mark Brörkens. Trace- und Zeit- Zusicherungen beim Programmieren mit Vertrag. Masters thesis. University of Oldenburg, Computer Science Department, January 2002. in German. (PDF, Sildes in PDF)

Mark Brörkens, Michael Möller. Jassda Trace Assertions, Runtime Checking the Dynamic of Java Programs. In Ina Schieferdecker, Hartmut König and Adam Wolisz (Eds.), Trends in Testing Communicating Systems, International Conference on Testing of Communicating Systems, Berlin, March 2002, pp. 39-48. (PDF)

Research into runtime checking of programs mainly concentrates on the Design by Contract concept, as proposed by Meyer for the programming language Eiffel. The goal is here to check whether a program fulfills certain conditions in certain states, i.e method entry and exit points. Jass (Java with assertions) tries to extend this to behavioural properties by adding trace assertion for dynamical checking (Jass 2). But the Jass approach is a precompiler attempt, so we cannot handle programs without its source code.
Jassda, the Jass Debug Architecture, is also designed to provide a trace assertion facility, but in contrast to the classic Jass 2 trace assertions these assertions are not precompiled into source code but are checked at runtime via the Java Debug Interface (JDI).

Michael Möller. Specifying and Checking Java using CSP. In Workshop on Formal Techniques for Java-like Programs - FTfJP’2002, Technical Report NIII-R0204. Computing Science Department, University of Nijmegen, 2002. (PDF, Slides in PDF)

Currently several approaches are done in applying formal techniques to the Java programming language. A new trend is to take dynamic behaviour into account when designing such techniques. To bring formal techniques to practical applications one often has to reduce the goal coming down from full verification to runtime checking. Jassda is a framework for performing such runtime checks at the bytecode level of Java. The Trace-Checker module of Jassda allows one to test the dynamic behaviour of multiple Java virtual machines by monitoring whether the trace of all relevant events is a member of the trace semantics of a given CSP process or not.
In this paper we present the CSP dialect that is used to specify a set of allowed traces for Java programs. The underlying semantics allow partial specification of distributed Java programs and to recombine them while preserving properties.

Mark Brörkens, Michael Möller. Dynamic Event Generation for Runtime Checking using the JDI. In Klaus Havelund and Grigore Rosu (Eds.), Proceedings of the Federated Logic Conference Satellite Workshops, Runtime Verification. Electronic Notes in Theoretical Computer Science 70.4, Copenhagen, July 2002. (PDF, Powerpoint slides)

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to the compilation or by modifying the target code, e.g. Java byte code, before running the program.
The Jassda framework and tool enable runtime checking of Java programs against a CSP-like specification. For generating events it uses the Java Debug Interface (JDI) and thus no modifications to the code are necessary. Another advantage is that events are generated on demand, i.e. dynamically at runtime it is determined which events to generate for the current debug run without modifying the program itself. This paper shows how this event generation is done by the Jassda framework.