本發(fā)明公開了一種形式化驗證系統(tǒng)，包括SEDS建模模塊，用于依據(jù)電子數(shù)據(jù)表單規(guī)范文件建立SEDS模型；模型轉換模塊用于將SEDS模型轉換為適合模型檢查的形式化模型；性質(zhì)規(guī)約模塊用于對SEDS模型的功能邏輯的性質(zhì)進行形式化描述；形式化驗證模塊用于對形式化模型和所描述的功能邏輯性質(zhì)進行形式化驗證，得到驗證結果。本發(fā)明通過將SEDS模型轉換為形式化模型，對SEDS模型的功能邏輯的性質(zhì)進行形式化描述，對形式化模型和性質(zhì)描述進行形式化驗證，以從數(shù)學推理角度對SEDS的功能邏輯實現(xiàn)檢查，進而保障軟件的正確性和可靠性，同時用戶還可以根據(jù)驗證結果發(fā)現(xiàn)功能邏輯中存在的沖突或缺陷，并對SEDS模型中的錯誤進行修正。

技術領域

本發(fā)明主要涉及形式化驗證領域，尤其涉及一種形式化驗證系統(tǒng)。

背景技術

隨著軍事戰(zhàn)略的不斷調(diào)整和航天技術的不斷進步，SEDS(Space Electronic DataSheet，電子數(shù)據(jù)表單)成為SOIS(spacecraft onboard interface services,航天器星載接口業(yè)務)領域的工作重點。針對目前實現(xiàn)的星載軟件快速集成和測試的需求，SEDS可以通過工具自動生成星載軟件、測試用例以及相關文檔，從而減少了星載軟件集成、測試、維護時間，并保證各個研制階段數(shù)據(jù)的一致性，并且SEDS一旦形成，其應用通常貫穿于項目開發(fā)和運行的各個階段。因此，SEDS的功能邏輯一致性和完備性顯得尤為重要。

目前主要采用的是測試方式來驗證SEDS的功能邏輯正確性。然而，測試方式只能以列舉方式來測試SEDS的功能邏輯是否正確，并不能涵蓋SEDS的所有狀態(tài)，因此無法保障軟件的正確性和可靠性。

發(fā)明內(nèi)容

本發(fā)明的目的是針對上述現(xiàn)有技術的不足提出的一種形式化驗證系統(tǒng)，該目的是通過以下技術方案實現(xiàn)的。

具體的，本發(fā)明提出了一種形式化驗證系統(tǒng)，包括：

SEDS建模模塊，用于依據(jù)電子數(shù)據(jù)表單規(guī)范SEDS Shema文件建立SEDS模型；

模型轉換模塊，用于將所述SEDS模型轉換為適合模型檢查的形式化模型；

性質(zhì)規(guī)約模塊，用于對所述SEDS模型的功能邏輯的性質(zhì)進行形式化描述；

形式化驗證模塊，用于對所述形式化模型和所描述的功能邏輯性質(zhì)進行形式化驗證，得到驗證結果。

優(yōu)選的，如上所述的形式化驗證系統(tǒng)，所述SEDS建模模塊，具體用于通過Eclipse建模框架讀取所述SEDS Shema文件建立SEDS模型。

優(yōu)選的，如上所述的形式化驗證系統(tǒng)，所述模型轉換模塊，具體用于通過語言解析工具從所述SEDS模型中移除與功能邏輯的性質(zhì)無關的信息后，再利用轉換規(guī)則將其轉換為形式化模型。

優(yōu)選的，如上所述的形式化驗證系統(tǒng)，所述性質(zhì)規(guī)約模塊包括一致性規(guī)約單元和完備性規(guī)約單元；

所述一致性規(guī)約單元，用于利用預設的性質(zhì)描述語言，對所述SEDS模型的功能邏輯的一致性進行形式化描述；

所述完備性規(guī)約單元，用于利用預設的性質(zhì)描述語言，對所述SEDS模型的功能邏輯的完備性進行形式化描述。

優(yōu)選的，如上所述的形式化驗證驗證系統(tǒng)，所述一致性的形式化描述用于檢查所述SEDS模型的功能邏輯是否存在矛盾。

優(yōu)選的，如上所述的形式化驗證系統(tǒng)，所述完備性的形式化描述用于檢查所述SEDS模型的功能邏輯是否能夠完全無遺漏地刻畫所要描述的功能。

優(yōu)選的，如上所述的形式化驗證系統(tǒng)，所述形式化驗證模塊，具體用于將所述形式化模型和所述所描述的功能邏輯性質(zhì)輸入模型檢測工具，以使所述模型檢測工具對所述形式化模型和所描述的功能邏輯性質(zhì)進行形式化驗證并輸出驗證結果。