Model-based testing (MBT) is applied for the verification of simple simulation models used in modeling & simulation for decision-making. It is found that MBT of simulation models is not discussed much in literature, and that existing case studies on this topic do not give guidelines for test model design. It is established that testing simulation models is a difficult problem, as simulation models have many states, a time component, reactiveness, and inherent stochasticity. It is hypothesized that MBT could lead to more efficient and effective testing, and could fit within a modular approach to verification of simulation models. A focus is made on verification that discrete-event simulation models meet their functional requirements, by using automated test packages. Options for test model design are explored in three case studies where automated test suites are developed for three simple simulation models that form the systems under test (SUT). Options from existing taxonomies are first selected for this, based on their relevance to the properties of simulation models that make dynamic verification difficult. In the process, an existing MBT software tool is selected and evaluated. The main aspects of MBT that are explored are: nondeterministic test models and SUTs, transition-based test models, online and reactive test execution, specification of oracles at different levels, time advancement of the SUT, the distinction between black-box and white-box approaches, and the problem of test abstraction. Examples are made where the test model, an extended finite state machine (EFSM), is an abstract version of the SUT, that includes its most relevant state transitions. An approach to testing is used, where the test model follows the SUT’s state and selects relevant assertions accordingly. This approach limits the use of stochasticity in the test model, that is often done in MBT. It is found that MBT can be useful for three types of dynamic verification: of the dynamic behavior, of the (end) results, and of the response to inputs. The first type is explored with a step-by-step approach where oracles are checked after each time advancement in the SUT. The second type is implemented without the use of MBT techniques, by extending the functionality of an existing MBT tool to allow for analysis of multiple simulation runs. The third type is not explored but approaches for it are defined. The project shows the feasibility of MBT of simulation models and shows different options for test model design. Not discussed are the adequacy of the developed test packages in detecting faults, and the efficiency, effectiveness and quality of MBT for simulation models in general.