In order to formally validate cyber-physical systems, analytically tractable models of human control are desirable. While those models can be abstracted directly from human data, limitations on the amount and reliability of data can lead to overfitting and lack of generalization. We introduce a methodology for deriving formal models of human control of cyber-physical systems based on the use of cognitive models. Analytical models such as Markov models can be derived from an instance-based learning model of the task built using the ACT-R cognitive architecture. The approach is illustrated in the context of a robotic control task involving the choice of two options to control a robotic swarm. The cognitive model and various forms of the analytical model are validated against each other and against human performance data. The current limitations of the approach are discussed as well as its implications for the automated validation of cyber-physical systems.