UML state machine diagram driven runtime verification of Java programs for message interaction consistency

Abstract

In object-oriented programs, we often need to set some restrictions on the temporal orders of the message receiving for objects, which forms a class of safety requirements. In this paper, we use UML state machine diagrams as design specifications, and present an approach to runtime verification of Java programs, which is focused on the temporal order of message receiving based consistency verification between the behavior of state machine diagrams and the program execution traces. In the approach, we first instrument the program under verification so as to gather the program execution traces related to a given state machine diagram. Then we drive the instrumented program by random test cases so as to generate the program execution traces. Finally we check if the collected program execution traces are consistent with the behavior of the state machine diagram, which means that the temporal orders of the message receiving occurring in the program traces are consistent with the ones occurring in the state machine diagram. Our approach can be used to detect not only the program bugs resulting from the wrong temporal orders of message receiving, but also the imperfect state machine models constructed in reverse engineering for legacy systems, and leads to a testing tool which may proceed in a fully automatic fashion.