由于信息技术的发展和国家政策的支持,各高校纷纷开始虚拟仿真实验教学平台的建设。但由于所建设的大部分实验教学平台搭载的实验要求单一,且没有对应的线上自动判别功能,导致学生之间相互抄袭严重,教师也难以真正掌握学生的实验学习情况。论文分析了国内外虚拟仿真实验教学平台的发展现状,指出了当前平台的不足之处,并结合工控系统PLC程序验证方法、离散事件动态系统等技术理论,在已开发的自动控制类虚拟仿真实验教学平台上提出了 PLC程序判别功能的设计方案。主要工作如下:论文首先针对实验教学中实验要求单一、学生之间相互抄袭严重的现状,提出了课程实训虚拟场景实验要求随机生成的两种方法。一是基于元规则的实验要求随机生成方法;二是基于控制逻辑的实验要求随机生成方法。用以改变传统实验教学的缺陷,提升教学质量。其次在实验要求随机生成的基础上,利用定理证明器Coq对实验要求进行分析与定理证明,将已分析证明的控制状态在Stateflow上进行程序判别模型的搭建。同时为保证模型的正确性与可行性,论文采用了 Simulink/Matlab进行模型的仿真测试。最后,将仿真测试结果正确的判别模型编译为C代码,在其中加入网络通讯模块,将其封装成具有程序判别功能的微服务模块,并将微服务模块部署在实验教学平台上,通过实际的PLC程序控制虚拟实训场景来进行判别功能的测试。在实验教学平台中的测试结果表明,所开发的PLC程序判别功能可对实际PLC程序的逻辑规则进行准确判别和纠错。该设计方案能够真正的满足实际实验教学的需要;也证明了定理证明和模型检测相结合的形式化程序判别方法,在自动控制类实验教学平台上的可行性。