In order to ensure a seamless execution of digital twins, functional properties such as absence of deadlocks and livelocks, quantitative dynamic properties such as overall model execution speed and erratic execution times of individual model components, other standard desirable properties such as model throughput and tailor-made properties based on user specifications needs to be validated. In this study, we aim to design and execute a complete methodology and appropriate tooling for model checking and validation of the aforementioned properties and a proof-of-concept encompassing the different industrial digital twin cases.