本发明属于系统形式化建模与验证领域和智能排课技术领域，公开了一种智能排课建模验证方法、系统，所述智能排课建模验证方法包括：使用MSVL语言对排课系统的功能需求分析进行系统建模，自定义业务实体的MSVL数据结构及算法，将核心模块编写为MSVL代码；使用命题投影时序逻辑PPTL公式描述系统期望性质，包括对课程、教师、教室、学生的约束在内的排课业务性质；使用PPTLCheck对系统MSVL代码与PPTL性质公式进行自动的模型检测验证。本发明能够在满足学校教学管理要求的前提下，较为合理地利用教学资源编排课表，且及时响应教学资源和约束条件的变化，是排课系统和基于MSVL的验证方法的成功结合。