Jassda

Jassda(Java with assertions Debugger Architecture) is a tool for checking trace- and time-assertions of Java applications.

Introduction

Todays software systems become more and more complex. But the complexity is not the only problem to handle. Software also gets more distributed, e.g. as consequence of the growing number of web-based software systems. This results in a special interest in tracking the correctness of these software systems, but formal specification techniques and especially static checking of programs against those specification are the topic of current research, and currently is often not applicable for large software systems.

The trace assertions approach extends the traditional Design by Contract concept by dealing with the dynamic order of such component uses: which component may use which other component and what third component has possibly to be used before. So we are interested in when the use of a component begins and when it ends. For this reason the entry and exit points become events that we want to observe, and therefore a program run emits a sequence, i.e. a trace, of those events.

To describe the desired behaviour of a program we define CSP-like parallel processes that specify all those traces that we want to allow. In some cases certain events may not matter for the correct execution of a program, so the events of interest are restricted to the set of events mentioned in the specifying process, called the alphabet of the process. This alphabet helps to reduce the amount of events to be emitted by the program, since this might be an important performance aspect as shows. Jassda does not precompile Java source code to emit and check events but uses the Java Debug Interface (JDI) to do this. Therefore Jassda does not have to modify the source code of the observed Java program.

Development

Jassda was developed by Dipl.-Inform. Mark Brörkens at his mastersthesis. The work was supported by the Correct System Design Group. The group also continues the work on Jassda in the context of the ForMooS Project. It is an opensource-project at SourceForge.net.

Documentation

• Libraries that are used by Jassda
• Links to sites that have been useful during developing Jassda
• Publications about Jassda