Informal design artefacts allow end-users and nonexperts to contribute to software design ideas and development. In contrast, software engineering techniques such as modeldriven development support experts in ensuring quality properties of the software they propose and build. Each of these approaches have benefits which contribute to the development of robust, reliable and usable software, however it is not always obvious how best to combine these two. In this paper we describe a novel technique which allows us to use informal design artefacts, in the form of ideation card designs, to generate formal models of IoT applications. To implement this technique, we created the Cards-to-Model (C2M) tool which allows us to automate the model generation process. We demonstrate this technique with a case study for a safety-critical IoT application called “Medication Reminders”. By generating formal models directly from the design we reduce the complexity of the modelling process. In addition, by incorporating easy-to-use informal design artefacts in the process we allow non-experts to engage in the design and modelling process of IoT applications