Where academic tradition
meets the exciting future

Using UML Models and Formal Verification in Model-Based Testing

Qaisar Malik, Dragos Truscan, Johan Lilius, Using UML Models and Formal Verification in Model-Based Testing. In: Roy Sterritt, Brandon Eames, Jonathan Sprinkle (Eds.), 17th IEEE Intl. Conference on Engineering of Computer-Based Systems (ECBS 2010), 50–56, IEEE Computer Society, 2010.

http://dx.doi.org/10.1109/ECBS.2010.13

Abstract:

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.

BibTeX entry:

@INPROCEEDINGS{inpMaTrLi10a,
  title = {Using UML Models and Formal Verification in Model-Based Testing},
  booktitle = {17th IEEE Intl. Conference on Engineering of Computer-Based Systems (ECBS 2010)},
  author = {Malik, Qaisar and Truscan, Dragos and Lilius, Johan},
  editor = {Sterritt, Roy and Eames, Brandon and Sprinkle, Jonathan},
  publisher = {IEEE Computer Society},
  pages = {50–56},
  year = {2010},
  keywords = {Model-based testing, UML-based testing, Event-B},
}

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB), Software Engineering Laboratory (SE Lab)

Publication Forum rating of this publication: level 1

Edit publication