基于前后斷言法的溫度控制系統程序驗證

鄧雪峰 葛躍 王建偉 馮靈清 侯思悅

摘? ?要：溫度控制系統已經廣泛地應用于各個領域，溫度控制系統對可靠性要求較高，一般來說，溫度控制系統的故障將導致災難性的后果。溫度系統的設計直接影響了系統的可靠性，文章利用前后斷言法對溫度控制系統的設計進行驗證，結論表明，該方法可以保證溫度控制系統設計的正確性，保證系統可靠運行。

關鍵詞：溫度控制系統;程序驗證;前后斷言

隨著物聯網技術的發展，監控系統在工農業等多個領域，能夠實現對環境的監測與控制功能。溫度作為環境信息中最普遍的一個指標，在控制系統中常常作為主要的控制參數使用。溫度控制系統[1]一般由溫度傳感器與智能控制系統共同構成，往往控制著系統至關重要的部分，其錯誤執行一般來說會造成系統的嚴重問題[2-3]，因此，對溫度控制系統的控制程序設計要保證正確性。前后斷言法[4]是由Floyd提出的一種對程序流程圖正確性驗證的方法，本文針對溫度控制程序流程中的關鍵部分進行分析，利用前后斷言法保證流程設計的正確性。

1? ? 溫度控制系統程序設計

1.1? 溫度控制系統簡介

溫度控制系統一般由溫度檢測傳感器、系統時鐘、鍵盤裝置、系統顯示報警裝置、被控制的部分和智能控制模塊組成。其中，（1）溫度檢測裝置：一般主要采用數字化的溫度芯片測量溫度，采用熱敏電阻的方式提升了系統的精度和可靠性，因此，成為溫度控制系統的測量溫度的主要器件。（2）系統時鐘及輸入鍵盤等裝置：用來控制系統的正常運行，設定系統運行的參數。（3）系統顯示報警裝置：可采用LED屏幕及聲光報警器，顯示當前系統的狀態信息以及在溫度異常時產生相應的信號。（4）被控制部分：主要是在系統溫度達到一定范圍時，系統輸出一系列的控制信息，以驅動相應的設備進行溫度調節。（5）智能控制模塊：根據系統的設計需求，可以采用單片機或高速的智能芯片，控制系統運行，一般來說，系統的主控程序運行于此。

1.2? 溫度控制系統執行流程

溫度控制系統典型的一個執行流程如下：（1）系統初始化。（2）檢測溫度傳感器。（3）啟動溫度傳感器進行溫度轉換。（4）系統延時。（5）讀取溫度傳感器中的溫度信息。（6）顯示溫度信息。（7）完成智能控制、報警等其他操作。

在這個過程中，系統初始化完成系統的初始設置，過程結束后，系統通過總線檢測溫度傳感器信息，檢測到溫度傳感器信息后，啟動溫度傳感器進行溫度轉換，系統延時階段等待溫度轉換完成，而后通過讀取溫度傳感器中寄存器的內容，獲取溫度信息，最后，達到利用溫度信息實現對系統進行控制、報警等功能。

2? ? 基于前后斷言法的控制程序驗證

2.1? 基本原理介紹

前后斷言法的基本原理為在語句S前添加前提條件P且在語句S后增加結論斷言Q，表示為P{S}Q。其中，P被稱為前置斷言，Q被稱為后置斷言。若程序執行前，P為真，程序S執行可終止，并且程序終止后如果Q是真的，此時稱S對于前置斷言P與后置斷言Q是完全正確的。一個程序的完全正確性一般分成兩部分證明：（1）程序的部分正確性證明，主要證明在程序S終止的情況下，基于前置斷言P可以推出后置斷言Q的正確性。（2）程序S的可終止性的證明，Folyd采用的是一種基于良序集的證明方法。

2.2? 程序驗證過程

基于上述系統執行流程，一個溫度監測程序執行的流程是一個順序過程，由P{S1}R1，R1{S2}R2……Rn{Sn}Q。證明第一個模塊P{S1}R1，其中，R1可以作為第二個模塊執行的前提，如此可以依次證明以后的各個部分，直至Rn{Sn}Q，這樣可以證明整個程序執行流程的正確性。對其中一個模塊進行程序驗證，可以分別對該程序模塊進行部分正確性驗證與可終止性證明。

部分正確性驗證的證明過程主要包括建立斷言、建立檢驗條件、證明檢驗條件等;而模塊的終止性只涉及循環過程，一般證明在循環過程中的一個斷言為“良斷言”完成終止性的證明。

3? ? 程序模塊驗證實例

以上證明過程的敘述，程序可以分別對每個模塊進行證明，由于模塊順序執行，前一個模塊證明的后置斷言可以作為下一個模塊的前置斷言，所以本部分研究以溫度傳感器中一個溫度控制實例闡述溫度控制程序正確性證明的過程，其他部分各個模塊可以按類似方法分別證明。

3.1? 溫度控制實例說明

以常見的溫度報警控制過程為例，說明溫度控制主程序的執行過程，流程圖如圖1所示。

其中，X1，X2分別代表系統預置的最高溫度與最低溫度界限，T1，T2為系統設計的條件變量，用于臨時存儲這兩個界限信息;C代表控制信息，用以發送到相應的控制器件，Con為控制信息存儲的臨時變量，C=﹣1，0，1分別代表溫度低于下界提供加熱控制、溫度正常、溫度高于上界提供冷卻控制;程序只列出一次控制過程，系統實際運行是循環執行，多次反復執行此過程。

3.2? 控制過程證明

圖1展示的過程中，在各個模塊下分別加以標記從A到J，用以說明問題。不仿設本溫度監控系統用于一個溫室監測系統，因此，溫度范圍可以X1=25，X2=35;控制信息預置為0，代表溫度正常狀態;傳感器讀取的溫度信息tem，臨時變量Y來存儲溫度信息。

證明這個程序的過程如下。

3.2.1? 建立斷言

程序是為獲得溫度控制信息，因此，在程序斷點A與J處建立前后斷言。

前斷言，q（A）：X1=25∧X2=35∧Y=Tem∧Con=0。

后斷言，q（J）：C=Con。

3.2.2? 建立檢驗條件

對于溫度控制程序，所有的通路有：A->B->C，C->G->I，C->D->E->H->I，C->D->F->I，I->J。

對于通路A->B->C，X1=25∧X2=35∧Y=Tem∧Con=0X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧Con=0。

對于通路C->G->I，X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧Con=0X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧Y

對于通路C->D->E->H->I，X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧Con=0X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧Y>T2∧Con=1。

對于通路C->D->F->I，X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧Con=0X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧T1≤Y≤T2∧Con=0。

對于通路I->J，X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧（YT2∧Con=1 or T1≤Y≤T2∧Con=0）X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧（YT2∧Con=1 or T1≤Y≤T2∧Con=0）∧C=Con。

3.2.3? 驗證檢驗條件

對于通路A->B->C，由X1=25∧X2=35∧Y=Tem∧Con=0，且T1=X1∧T2=X2，因此，X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧Con=0成立。

對于通路C->G->I，C->D->E->H->I、C->D->F->I分別由YT2則Con=1，由T1≤Y≤T2則Con=0得出結論，因此，檢驗條件成立。

對于通路I->J，在通路C->G->I，C->D->E->H->I，C->D->F->I成立的前提下，I處由3個基本條件Con=-1 or Con=1 or Con=0，包含了當前系統運行的所有的情況，由C=Con賦值，可以得出檢驗條件此時也成立。

本段程序中無循環，因此，終止性一定滿足，故本模塊程序正確性得以驗證。

4? ? 結語

溫度控制系統是一種可靠需求較高的系統，本文分析了溫度控制系統運行的過程，對系統中主要控制溫度的程序進行了設計并建模，利用前后斷言法將系統中的模塊進行形式化驗證，從而保證系統程序設計的可靠性。

[參考文獻]

[1]義凱，傅留虎，胡欣宇.智能溫度采集控制系統的研究[J].機械工程與自動化，2017（5）：15-16.

[2]倉理.基于可靠性的連鑄溫度控制系統設計[J].鑄造技術，2013（12）：1765-1767.

[3]葉盛.低成本高可靠性溫度監測與控制系統的研制及應用[J].實驗室研究與探索，2002（1）：74-76.

[4]伯格，H K.程序驗證和規范的形成方法[M].北京：科學出版社，1988.

Program verification of temperature control system based on pre-and post-assertion method

Deng Xuefeng， Ge Yue， Wang Jianwei， Feng Lingqing， Hou Siyue

（College of Information Science and Engineering， Shanxi Agricultural University， Taigu 030800， China）

Abstract：The temperature control system has been widely used in various fields. The temperature control system has high reliability requirements. Generally speaking， the failure of the temperature control system will lead to disastrous consequences. The design of the temperature system directly affects the reliability of the system. In this paper， pre-and post-assertion method is used to verify the design of the temperature control system. The results show that this method can ensure the correctness of the design of the temperature control system and ensure the reliable operation of the system.

Key words：temperature control system; program verification; pre-and post-assertion method