[發明專利]基于算術表達式的MSVL柱面計算方法和系統

有效

• 申請號: 201210038404.0
• 申請日: 2012-02-20
• 公開（公告）號: CN102646053A
• 公開（公告）日: 2012-08-22
• 發明（設計）人: 段振華;張南;李潔;田聰;王小兵
• 申請（專利權）人: 西安電子科技大學
• 主分類號: G06F9/46
• 分類號: G06F9/46;G06F9/54
• 代理公司: 陜西電子工業專利中心 61205
• 代理人: 程曉霞;王品華

技術領域

本發明屬于計算機系統形式化建模與驗證技術領域，主要涉及用形式化的方法對并行程序設計系統進行建模與驗證，具體是一種基于算術表達式的MSVL柱面計算方法和系統，可用于多核并行計算程序設計的建模與驗證。

技術背景

時序邏輯作為一種系統建模與驗證工具已廣泛應用于軟件工程、數字電路設計等領域。時序邏輯主要有三大分支：線性時序邏輯(ITL)，分支時序邏輯(CTL)以及區間時序邏輯(ITL)。投影時序邏輯(PTL)對ITL進行了擴展，時序邏輯語言MSVL是PTL的一個可執行子集，是一個集建模(Modeling)、仿真(Simulation)和驗證(Verification)為一體的時序邏輯程序設計語言，它將系統的建模與性質的描述統一于同一邏輯框架內，通過模型檢測技術驗證系統的性質。

自上世紀70年代，大量的基于區間或實時模型的單進程的并行或實時編程語言被提出，如帶有進程代數共享的CSP和CCS，都是典型的描述和驗證實時系統的語言，但是這些語言都是不可執行的。時序邏輯是一種用于描述和驗證實時系統實時性的重要方法，很多基于時序邏輯的編程語言都可以描述和證明同一邏輯框架下的程序。Cactus基于分支時間時序邏輯，XYZ/E，THLP，Chronolog，Tempura以及Tokio基于區間時序邏輯，TLA也是一種基于時序邏輯行為的描述語言。然而，這些語言更多地是用來描述和驗證，而不是開發實時系統程序。上述大多數的語言針對的都是單進程，用來解決交錯或真實時模型下的實時進程，不能夠直接處理多進程編程語言。

一個并行程序有多個進程組成，并且每個進程都是一個序列程序(sequential?program)，擁有各自的局部變量和語句，因此并行程序比單個程序更難處理。多進程程序設計或多核并行程序設計對于程序員開發并發程序是一項巨大的挑戰，因此，研究基本的多進程程序設計技術以及開發相關的支持工具(例如模型檢測器)以及理論證明均是計算機系統形式化建模與驗證技術領域的客觀需要，本發明正是在這方面進行的研究和創新。和上述形式化方法相比，MSVL具有顯著的優勢。因為MSVL是一個時序邏輯編程語言，有三種執行模式：建模，仿真和驗證，所以稱為建模仿真驗證語言(Modeling?Simulation?Verification?Language，即MSVL)。作為一種形式化的工具，MSVL可以用于對多核并行程序設計系統進行建模與驗證。但是目前MSVL的基本時序區間表達式還局限于正整數，描述能力和表達能力弱，應用不夠靈活，不能夠根據問題的不同用時序表達式和算術表達式來替代，適應面太窄。現有的MSVL缺乏一種有效的時序區間描述方法，這嚴重地限制了MSVL對并行多核程序設計系統的描述能力。

本發明項目組對國內外專利文獻和公開發表的期刊論文檢索，尚未發現與本發明密切相關和一樣的報道或文獻。

發明內容

本發明針對現有技術中時序區間表達式的描述能力和表達能力弱，應用范圍窄的技術問題，提供一種算術表達式和時序表達式均可表示時間區間，描述表達能力強，使進程的執行更加準確且可控的基于算術表達式的MSVL柱面計算方法和系統。

本發明是一種基于算術表達式的MSVL柱面計算方法，屬于系統形式化建模與驗證技術領域，對MSVL程序進程模塊進行仿真，建模和驗證，本發明定義多核并行程序語法，基于該多核并行程序語法和MSVL語句聲明一個多核并行程序，在該多核并行程序中，不同的進程在各自的時序區間上執行，該執行是由進程的時序區間表達式控制的，進程的時序區間和主時間區間并行，各個進程的時序區間并行地圍繞主時間區間形成一個圓柱面狀模型；基于算術表達式的MSVL柱面計算流程包括有：

步驟1、定義多核并行程序語法，一個多核并行程序或由一個進程，即單進程組成，或由多個并行的進程組成，即由多個單進程并行組成；多核并行程序的語法定義為：

CCM::＝Single_Progress|CCM₁|||CCM₂

其中，CCM為多核并行程序，|||是連接不同并行進程的關鍵字，Single_Progress為單進程，CCM₁和CCM₂為相互并行的兩個多核并行程序；

一個進程包括進程的執行體和進程的時序區間表達式兩部分，單進程的語法定義為：

Single_Progress::＝φovl

其中，φ定義了進程的執行體，l為控制進程執行體φ執行的時序區間表達式，ov為連接進程執行體和時序區間表達式的關鍵字；