[發(fā)明專利]形式化驗證系統(tǒng)有效
| 申請?zhí)枺?/td> | 202010113873.9 | 申請日： | 2020-02-24 |
| 公開（公告）號： | CN111338948B | 公開（公告）日： | 2022-04-05 |
| 發(fā)明（設(shè)計）人： | 黃滟鴻;楊秀麗;史建琦;曹桂濤;郭欣 | 申請（專利權(quán)）人： | 華東師范大學(xué) |
| 主分類號： | G06F11/36 | 分類號： | G06F11/36 |
| 代理公司： | 北京辰權(quán)知識產(chǎn)權(quán)代理有限公司 11619 | 代理人： | 付婧 |
| 地址： | 200062 上*** | 國省代碼： | 上海;31 |
| 權(quán)利要求書： | 查看更多 | 說明書： | 查看更多 |
| 摘要： | |||
| 搜索關(guān)鍵詞： | 形式化 驗證 系統(tǒng) | ||
1.一種形式化驗證系統(tǒng)，其特征在于，包括：
SEDS建模模塊，用于依據(jù)電子數(shù)據(jù)表單規(guī)范SEDS Shema文件建立SEDS模型；
模型轉(zhuǎn)換模塊，用于將所述SEDS模型轉(zhuǎn)換為適合模型檢查的形式化模型；
性質(zhì)規(guī)約模塊，用于對所述SEDS模型的功能邏輯的性質(zhì)進(jìn)行形式化描述；
形式化驗證模塊，用于對所述形式化模型和所描述的功能邏輯性質(zhì)進(jìn)行形式化驗證，得到驗證結(jié)果；所述形式化驗證為正確性驗證；
所述性質(zhì)規(guī)約模塊包括一致性規(guī)約單元和完備性規(guī)約單元；
所述一致性規(guī)約單元，用于利用預(yù)設(shè)的性質(zhì)描述語言，對所述SEDS模型的功能邏輯的一致性進(jìn)行形式化描述；
所述完備性規(guī)約單元，用于利用預(yù)設(shè)的性質(zhì)描述語言，對所述SEDS模型的功能邏輯的完備性進(jìn)行形式化描述。
2.如權(quán)利要求1所述的形式化驗證系統(tǒng)，其特征在于，所述SEDS建模模塊，具體用于通過Eclipse建?？蚣茏x取所述SEDS Shema文件建立SEDS模型。
3.如權(quán)利要求1所述的形式化驗證系統(tǒng)，其特征在于，所述模型轉(zhuǎn)換模塊，具體用于通過語言解析工具從所述SEDS模型中移除與功能邏輯的性質(zhì)無關(guān)的信息后，再利用轉(zhuǎn)換規(guī)則將其轉(zhuǎn)換為形式化模型。
4.如權(quán)利要求1所述的形式化驗證系統(tǒng)，其特征在于，所述一致性的形式化描述用于檢查所述SEDS模型的功能邏輯是否存在矛盾。
5.如權(quán)利要求1所述的形式化驗證系統(tǒng)，其特征在于，所述完備性的形式化描述用于檢查所述SEDS模型的功能邏輯是否能夠完全無遺漏地刻畫所要描述的功能。
6.如權(quán)利要求1所述的形式化驗證系統(tǒng)，其特征在于，所述形式化驗證模塊，具體用于將所述形式化模型和所述所描述的功能邏輯性質(zhì)輸入模型檢測工具，以使所述模型檢測工具對所述形式化模型和所描述的功能邏輯性質(zhì)進(jìn)行形式化驗證并輸出驗證結(jié)果。
7.如權(quán)利要求6所述的形式化驗證系統(tǒng)，其特征在于，所述驗證結(jié)果包括模型滿足性質(zhì)的結(jié)果和模型不滿足性質(zhì)的結(jié)果；
當(dāng)所述驗證結(jié)果為模型不滿足性質(zhì)時，所述模型檢測工具還會輸出反例結(jié)果，用戶可以根據(jù)所述反例結(jié)果對所述SEDS模型進(jìn)行修正和改進(jìn)。
該專利技術(shù)資料僅供研究查看技術(shù)是否侵權(quán)等信息，商用須獲得專利權(quán)人授權(quán)。該專利全部權(quán)利屬于華東師范大學(xué)，未經(jīng)華東師范大學(xué)許可，擅自商用是侵權(quán)行為。如果您想購買此專利、獲得商業(yè)授權(quán)和技術(shù)合作，請聯(lián)系【客服】
本文鏈接：http://www.17sss.com.cn/pat/books/202010113873.9/1.html，轉(zhuǎn)載請聲明來源鉆瓜專利網(wǎng)。
