Cyber attacks on Industrial Control Systems (ICSs) are becoming increasingly sophisticated, undermining the ability of these systems to manage critical processes and compromising the availability of key public infrastructure. Detecting system anomalies is an important element in the identification of cyber attacks, allowing the rapid deployment of crucial incident-response activities. In this paper, we introduce a novel anomaly detection approach that integrates SPIN model checking into ICS environments to detect anomalies in live system data. Our approach uses the application code extracted from Programmable Logic Controllers (PLCs) to generate the dynamic system model, requiring only a small amount of test data to validate their design. We evaluate our approach by generating models using a representative physical hydroelectric dam testbed containing real PLCs. These models are used to analyse synthetic data containing potential irregularities that could occur within the dam as a result of false data injection attacks. Our approach was shown to identify anomalies and verify normal system behaviour. Our evaluation shows that the models achieved high performance while maintaining explainability and delivering metrics of 99.99% precision, 99.05% recall, a 99.52% F1-score, and 99.05% accuracy.