Model-Based Testing (MBT) is a promising technology to extend test coverage beyond manually crafted tests, by automatically creating more, longer, and more diverse test cases, with less effort, from abstract models of the required behavior. When the models used for MBT are correct, the test cases are provably valid as well. TNO-ESI and ASML have been working on realizing MBT. With MBT, the hope is that the amount of time spent on creating System-of-System tests is reduced, while drastically increasing test coverage. Currently, the correctness of the models used for MBT is not analyzed. In this thesis, the aim is to introduce model checking for analysis of BPMN models. For model checking, mCRL2 is introduced as a verification back-end for the formal models used for MBT. Additionally, an easy-to-use property language is introduced and the results of model checking are translated back to the notation of BPMN models.