Formal Control Synthesis via Simulation Relations and Behavioural Theory for Discrete-Time Descriptor Systems