MSVL Modeling And Verification Of Course Arrangement System

Course scheduling is the basic work of educational administration activities in colleges,which is the key to guaranteeing teaching order.The manual scheduling mode has some shortcomings such as slow speed,high error rate,and heavy workload.In order to respond to the changes in teaching resources and constraints timely,the computer course scheduling system is often used to complete course scheduling.In practical applications,the results of the schedule arrangement generated by the course arrangement system need to be manually reviewed,otherwise it is easy to cause conflicts in the arrangement of courses,which will lead to serious teaching accidents,thus affecting the quality of teaching.Manual review also has problems such as heavy workload and error-proneness.At the same time,it requires auditors to have rich experience in course arrangement.Whether the results of the course arrangement meets the requirements of teaching management can actually be attributed to whether the algorithm of the course arrangement meets the properties of the conventional software and the properties of the course arrangement.Formal verification uses formal methods to verify computer software and hardware systems to judge whether the system meets the expected properties.It has been widely used in the field of safety-critical systems.This thesis uses the modeling,simulation and verification language MSVL to verify the course arrangement system,hoping to improve the safety of the system and the quality of the schedule.In this thesis,model checking technology is applied to a commercial intelligent course arrangement Java system,and a modeling and verification method for course arrangement system based on MSVL is proposed.The specific process of this method is as follows:Firstly,analyze the functional requirements of the business scenario of the course arrangement system,use the MSVL language to model the system,customize the MSVL data structure and algorithm of the business entity,and convert the Java code of the core module into MSVL code;Secondly,the expected properties of the system is summarized as the properties of conventional software and the properties of scheduling business,and the PPTL formula is used to describe the security properties,reliability properties,teachers,classrooms,students,and time constraints of the system;Then,PPTLCheck is used to check and verify the MSVL code and PPTL property formula automatically.The results show that the course scheduling system can meet the properties of conventional software and course scheduling business,and there are no problems in the basic business logic;Finally,the three validators,PPTLCheck,PAT and SPIN,are compared and analyzed.The modeling language MSVL used in this method is closer to a high-level programming language,and the PPTL used is more expressive,which is suitable for modeling and verification of the course arrangement system.