[發明專利]一種智能排課建模驗證方法、系統

在審

• 申請號: 202110498384.4
• 申請日: 2021-05-08
• 公開（公告）號: CN113434132A
• 公開（公告）日: 2021-09-24
• 發明（設計）人: 王小兵;王一寧;賀照易;于斌;段振華;趙亮;田聰;張南
• 申請（專利權）人: 西安電子科技大學
• 主分類號: G06F8/35
• 分類號: G06F8/35;G06F8/10;G06Q50/20
• 代理公司: 西安長和專利代理有限公司 61227
• 代理人: 何畏

本發明屬于系統形式化建模與驗證領域和智能排課技術領域，公開了一種智能排課建模驗證方法、系統，所述智能排課建模驗證方法包括：使用MSVL語言對排課系統的功能需求分析進行系統建模，自定義業務實體的MSVL數據結構及算法，將核心模塊編寫為MSVL代碼；使用命題投影時序邏輯PPTL公式描述系統期望性質，包括對課程、教師、教室、學生的約束在內的排課業務性質；使用PPTLCheck對系統MSVL代碼與PPTL性質公式進行自動的模型檢測驗證。本發明能夠在滿足學校教學管理要求的前提下，較為合理地利用教學資源編排課表，且及時響應教學資源和約束條件的變化，是排課系統和基于MSVL的驗證方法的成功結合。

技術領域

本發明屬于系統形式化建模與驗證領域和智能排課技術領域，尤其涉及一種智能排課建模驗證方法、系統。

背景技術

目前，在開展教學工作的過程中合理分配各類教學資源使教學工作順利展開，這一過程稱為排課。排課問題屬于教育資源分配管理問題，涉及到授課教師、課程、學生、教室和上課時間這五個關鍵要素。在進行資源分配時，若可分配的資源是無限的，為保證資源的順利分配通常可通過適當的增加資源來完成；若可分配的資源是有限的，需要優化分配計劃來保證順利分配。在排課問題中，學校的授課教師和教室等教學資源是相對有限的，所以解決排課問題的重點是在教學資源有限的情況下如何優化分配計劃，合理高效利用學校有限的教學資源，制定出合理高效的課表，提高教學質量和排課效率。傳統的排課采用人工排課的方式，教務人員根據學校的教學計劃和教學資源以及自身的排課業務經驗和排課過程中的具體觀察進行調整，最終得到排課結果。但隨著數據量的增大及約束條件的增加，人工排課已經無法完成編排高質量課表的目標。因此，亟需一種新的智能排課方法。

通過上述分析，現有技術存在的問題及缺陷為：傳統的排課采用人工排課的方式，但隨著數據量的增大及約束條件的增加，人工排課已經無法完成編排高質量課表的目標。

解決以上問題及缺陷的難度為：在使用MSVL程序對系統進行建模的過程中，由于現有的轉換工具中不含Java語言到MSVL的轉換器，所以需要采用手工轉換的方式建立MSVL程序模型對智能排課系統程序進行分析。這一手工轉換的方式無疑大大增加了驗證過程的工作量。

解決以上問題及缺陷的意義為：在MSVL統一模型檢測框架下對智能排課Java系統進行建模和驗證可在滿足學校教學管理要求的前提下，較為合理利用教學資源編排課表，并且可以及時響應教學資源和約束條件的變化，錯誤率小，效率高，降低了人力、財力和時間成本，提高排課系統安全性，保障課表編排質量。

發明內容

針對現有技術存在的問題，本發明提供了一種智能排課建模驗證方法、系統，尤其涉及一種基于MSVL的智能排課建模驗證方法、系統。

本發明是這樣實現的，一種智能排課建模驗證方法，所述智能排課建模驗證方法包括以下步驟：

步驟一，使用MSVL語言對排課系統的功能需求分析進行系統建模，自定義業務實體的MSVL數據結構及算法，將核心模塊編寫為MSVL代碼，實現了MSVL語言對系統進行建模，為驗證過程做了模型準備；

步驟二，使用命題投影時序邏輯PPTL公式描述系統期望性質，包括對課程、教師、教室、學生的約束在內的排課業務性質，實現了排課業務性質的抽象化且用PPTL公式進行描述，為驗證過程做了性質準備；

步驟三，使用PPTLCheck對系統MSVL代碼與PPTL性質公式進行自動的模型檢測驗證，結果表明排課系統能夠滿足排課業務性質，尚未發現基本業務邏輯存在問題。

進一步，步驟二中，所述業務性質需要滿足的約束條件分為硬約束條件和軟約束條件；其中，所述硬約束為課表必須滿足的基本規則，是指課程、授課教師、教室、上課學生、時間這五種核心要素之間的相互影響和制約，包括：

課程約束，同一節課在同一教學時間段內不能被重復安排；