[發(fā)明專利]一種智能排課建模驗(yàn)證方法、系統(tǒng)

在審

• 申請(qǐng)?zhí)枺?/td>: 202110498384.4
• 申請(qǐng)日: 2021-05-08
• 公開（公告）號(hào): CN113434132A
• 公開（公告）日: 2021-09-24
• 發(fā)明（設(shè)計(jì)）人: 王小兵;王一寧;賀照易;于斌;段振華;趙亮;田聰;張南
• 申請(qǐng)（專利權(quán)）人: 西安電子科技大學(xué)
• 主分類號(hào): G06F8/35
• 分類號(hào): G06F8/35;G06F8/10;G06Q50/20
• 代理公司: 西安長和專利代理有限公司 61227
• 代理人: 何畏

1.一種智能排課建模驗(yàn)證方法，其特征在于，所述智能排課建模驗(yàn)證方法包括以下步驟：

步驟一，使用MSVL語言對(duì)排課系統(tǒng)的功能需求分析進(jìn)行系統(tǒng)建模，自定義業(yè)務(wù)實(shí)體的MSVL數(shù)據(jù)結(jié)構(gòu)及算法，將核心模塊編寫為MSVL代碼；

步驟二，使用命題投影時(shí)序邏輯PPTL公式描述系統(tǒng)期望性質(zhì)，包括對(duì)課程、教師、教室、學(xué)生的約束在內(nèi)的排課業(yè)務(wù)性質(zhì)；

步驟三，使用PPTLCheck對(duì)系統(tǒng)MSVL代碼與PPTL性質(zhì)公式進(jìn)行自動(dòng)的模型檢測(cè)驗(yàn)證，結(jié)果表明排課系統(tǒng)能夠滿足排課業(yè)務(wù)性質(zhì)，尚未發(fā)現(xiàn)基本業(yè)務(wù)邏輯存在問題。

2.如權(quán)利要求1所述的智能排課建模驗(yàn)證方法，其特征在于，步驟二中，所述業(yè)務(wù)性質(zhì)需要滿足的約束條件分為硬約束條件和軟約束條件；其中，所述硬約束為課表必須滿足的基本規(guī)則，是指課程、授課教師、教室、上課學(xué)生、時(shí)間這五種核心要素之間的相互影響和制約，包括：

課程約束，同一節(jié)課在同一教學(xué)時(shí)間段內(nèi)不能被重復(fù)安排；

教師約束，一個(gè)教師在同一教學(xué)時(shí)間段內(nèi)只能上一節(jié)課；

教室約束，一個(gè)教室在同一教學(xué)時(shí)間段內(nèi)只能安排一節(jié)課；

學(xué)生約束，一個(gè)學(xué)生在同一教學(xué)時(shí)間段內(nèi)只能上一節(jié)課。

3.如權(quán)利要求2所述的智能排課建模驗(yàn)證方法，其特征在于，所述業(yè)務(wù)性質(zhì)需滿足的課程約束為：

變量propertyCheckingFlagOfCourse的值為1，表示同一門課的同一節(jié)次沒有被重復(fù)安排；命題np3定義為變量值不等于1，som(np3)表示在排課系統(tǒng)MSVL程序運(yùn)行區(qū)間內(nèi)的某一時(shí)刻np3成立。

4.如權(quán)利要求2所述的智能排課建模驗(yàn)證方法，其特征在于，所述業(yè)務(wù)性質(zhì)需滿足的教師約束為：

變量propertyCheckingFlagOfTeacher的值為1，表示一個(gè)老師在同一時(shí)間段只有一節(jié)課的上課安排；som(p4 and next np4)表示在排課系統(tǒng)MSVL程序的運(yùn)行區(qū)間內(nèi)將來的某一狀態(tài)p4成立，在下一狀態(tài)np4成立，則說明課表結(jié)果中一個(gè)老師在同一時(shí)間內(nèi)的課程安排沖突，其中next表示下一狀態(tài)；滿足該性質(zhì)表示排課系統(tǒng)不符合同一教師在同一時(shí)間段內(nèi)只上一節(jié)課的約束，不滿足該性質(zhì)則排課系統(tǒng)是滿足約束的。

5.如權(quán)利要求2所述的智能排課建模驗(yàn)證方法，其特征在于，所述業(yè)務(wù)性質(zhì)需滿足的教室約束為：

變量propertyCheckingFlagOfRoom的值為1，表示一個(gè)教室在同一時(shí)間段只有一節(jié)課的課程安排；som(p5 and next np5)表示在系統(tǒng)的運(yùn)行區(qū)間內(nèi)將來的某一狀態(tài)p5成立，在下一狀態(tài)np5成立，說明課表結(jié)果中一間教室的同一時(shí)間內(nèi)安排兩節(jié)課程，其中next表示下一狀態(tài)；滿足該性質(zhì)表示排課系統(tǒng)不符合一個(gè)教室在同一時(shí)間段只有一節(jié)課的課程安排的約束，不滿足該性質(zhì)則表示排課系統(tǒng)滿足約束。

6.如權(quán)利要求2所述的智能排課建模驗(yàn)證方法，其特征在于，所述業(yè)務(wù)性質(zhì)需滿足的學(xué)生約束為：

變量propertyCheckingFlagOfStudent值為1表示一個(gè)學(xué)生在同一時(shí)間段只能上一節(jié)課；命題p6定義為變量的值等于1，alw(p6)表示一個(gè)學(xué)生在同一時(shí)間段只能上一節(jié)課永遠(yuǎn)成立。

7.如權(quán)利要求1所述的智能排課建模驗(yàn)證方法，其特征在于，步驟三中，所述使用PPTLCheck對(duì)系統(tǒng)MSVL代碼與PPTL性質(zhì)公式進(jìn)行自動(dòng)的模型檢測(cè)驗(yàn)證，包括：

PPTLCheck接受PPTL公式和MSVL程序，也可以將PPTL公式附加在MSVL程序前面執(zhí)行，通過二者在驗(yàn)證器中的運(yùn)行結(jié)果來判斷排課系統(tǒng)MSVL模型是否滿足待驗(yàn)證性質(zhì)。