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