Model-driven system engineering is a practice also employed in the design of controllers for cyber-physical systems. The method allows controllers to be modelled and verified before they are implemented in software, allowing potential glitches and design flaws to be uncovered, before they emerge in the time and resource intensive testing phase. Some of the modelling formalisms used by the industry allow controllers to be automatically generated from models, which aides in the prevention of human error in the implementation of such systems. The question arises whether the behavior of the generated software components is equivalent to those of the specified models, as the semantics of such systems might not always be trivially deduced. The topic of this talk is about how to solve this problem. It will present a way to deduct the state-space from implemented software controllers, and the intricacies of this approach. It will give the context of where this question arose, and what its contribution can potentially be for the industry and in a general setting. It will conclude with a few examples to shows the approach in working order, and if you are still reading this, given there is enough time and interest in the subject a more interactive demonstration.