Model checking as well as model generation (aka model finding) are well-established methodologies for formally verifying properties of possibly time-evolving systems. In order to support the ontology development process in an incremental way, our thesis is that well-known model-generation tools can be adopted accordingly and provide major benefits for human ontology designers. In this work we evaluate pros and cons of applying an existing model checking and generation tool in this context.