Using UML Models and Formal Verification in Model-Based Testing

In this paper we present a model-based testing approach where we integrate UML, UML-B and the Qtronic test generator tool, with the purpose of increasing the quality of models used for test generation via formal verification. The architectural and behavioral models of the system under test (SUT) are specified in UML and UML-B, respectively. UMLB provides UML-like visualization with precise mathematical semantics. UML-B models are developed in a stepwise manner which are then automatically translated into Event-B specifications that can be proved using theorem provers. Once the formal models are proved, they are transformed into QML which is a modeling language used by the test generation tool.