Testing Meets Static and Runtime Verification

Jesus Mauricio Chimento, Wolfgang Ahrendt, Gerardo Schneider

Testing driven development (TDD) is a technique where test cases are used to
guide the development of a system. This technique introduces several advantages
at the time of developing a system, e.g. writing clean code, good coverage for
the features of the system, and evolutionary development. In this paper we show
how the capabilities of a testing focused development methodology based on TDD
and model-based testing, can be enhanced by integrating static and runtime
verification into its workflow. Considering that the desired system properties
capture data- as well as control-oriented aspects, we integrate TDD with (static)
deductive verification as an aid in the development of the data-oriented aspects,
and we integrate model-based testing with runtime verification as an aid in the
development of the control-oriented aspects. As a result of this integration, the
proposed development methodology features the benefits of TDD and model-based
testing, enhanced with better coverage regarding data aspects, and the validation
of the overall system with respect to the model, regarding the control aspects.