[發明專利]一種基于TMSVL的C語言實時系統運行形式化分析方法

在審

• 申請號: 201410330453.0
• 申請日: 2014-07-11
• 公開（公告）號: CN104111889A
• 公開（公告）日: 2014-10-22
• 發明（設計）人: 王小兵;蘇多鐸;段振華;趙亮;田聰;張南
• 申請（專利權）人: 西安電子科技大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京科億知識產權代理事務所(普通合伙) 11350
• 代理人: 湯東鳳

1.一種基于TMSVL的C語言實時系統運行形式化分析方法，其特征在于，所述方法包括如下步驟：

步驟1，在所述C語言實時系統源代碼中插入斷言語句，形成一個加入斷言語句后的源代碼程序；

步驟2，對所述加入斷言語句后的源代碼程序進行編譯，得到C語言實時系統的可執行文件；

步驟3，用TMSVL語言來描述待驗證性質變量在特定時間點上應該處于的狀態，形成一個TMSVL程序；

步驟4，TMSVL監控器啟動所述C語言實時系統的可執行文件，在執行的過程中，所述斷言語句記錄所述待驗證性質變量的實際信息；所述TMSVL監控器解釋執行所述TMSVL程序時通過一定的方式獲取所述待驗證性質變量的實際信息；

步驟5，所述TMSVL監控器解釋執行所述TMSVL程序并獲取到所述待驗證性質變量的實際信息后，與所述TMSVL語言描述的待驗證性質變量應該處于的狀態作對比，驗證C語言實時系統的實時性質是否滿足：

若所述待驗證性質變量的實際狀態信息符合所述待驗證性質變量應該處于的狀態，則判定為C語言實時系統的實時性質滿足；否則，則判定為C語言實時系統的實時性質不滿足。

2.根據權利要求1所述的一種基于TMSVL的C語言實時系統運行形式化分析方法，其特征在于，所述斷言語句為C語言語句或C語言函數。

3.根據權利要求1所述的一種基于TMSVL的C語言實時系統運行形式化分析方法，其特征在于，所述待驗證性質變量的實際信息包括所述待驗證性質變量的名稱、值、值所占存儲空間的大小以及值產生的時間。

4.根據權利要求1所述的一種基于TMSVL的C語言實時系統運行形式化分析方法，其特征在于，所述步驟4中，所述斷言語句將所述待驗證性質變量的實際信息輸出到文本文件中，所述TMSVL監控器解釋執行所述TMSVL程序時從所述文本文件中獲取所述待驗證性質變量的實際信息，具體實施步驟為：

步驟4.1，所述TMSVL監控器啟動所述C語言實時系統的可執行文件；

步驟4.2，在執行的過程中，當執行到所述斷言語句時，所述斷言語句將所述待驗證性質變量的實際信息記錄下來并輸出至文本文件中；

步驟4.3，執行過程完成后，所述TMSVL監控器開始解釋執行所述TMSVL程序，并從所述文本文件中獲取所述待驗證性質變量的實際信息。

5.根據權利要求1所述的一種基于TMSVL的C語言實時系統運行形式化分析方法，其特征在于，所述步驟4中，所述斷言語句將所述待驗證性質變量的實際信息記錄下來，并通過進程間通信中的匿名管道的方式傳遞給所述TMSVL監控器，具體步驟如下：

步驟4.1，利用TMSVL監控器啟動所述C語言實時系統的可執行文件，與此同時所述TMSVL監控器開始解釋執行所述TMSVL程序；

步驟4.2，執行的過程中，每執行一次所述斷言語句，所述斷言語句就把所述待驗證性質變量的實際信息寫入匿名管道中，所述TMSVL監控器解釋執行所述TMSVL程序時利用進程間通信相關語句對所述匿名管道實施監控，從所述匿名管道中獲取所述待驗證性質變量的實際信息。