Testing Temporal Logic Properties in Distributed Systems

Based on the notion of event-based behavioral abstraction (EBBA) we specify properties of object-oriented distributed systems in linear time temporal logic. These properties are then observed at system run-time and it is checked whether or not the system violates the specified behavioral constraints. In our approach, several steps in the testing process can be automized: instrumenting the source code, constructing test-oracles and generating an observer. Taking an industrial example as basis, we discuss how our proposal can be integrated into the software design- and testing process.