Modeling cyber-physical systems for automatic verification