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

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

關鍵詞：溫度控制系統(tǒng);程序驗證;前后斷言

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

1? ? 溫度控制系統(tǒng)程序設計

1.1? 溫度控制系統(tǒng)簡介

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

1.2? 溫度控制系統(tǒng)執(zhí)行流程

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

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

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

2.1? 基本原理介紹

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

2.2? 程序驗證過程

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

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

3? ? 程序模塊驗證實例

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

3.1? 溫度控制實例說明

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

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

3.2? 控制過程證明

圖1展示的過程中，在各個模塊下分別加以標記從A到J，用以說明問題。不仿設本溫度監(jiān)控系統(tǒng)用于一個溫室監(jiān)測系統(tǒng)，因此，溫度范圍可以X1=25，X2=35;控制信息預置為0，代表溫度正常狀態(tài);傳感器讀取的溫度信息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得出結(jié)論，因此，檢驗條件成立。

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

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

4? ? 結(jié)語

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

[參考文獻]

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

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

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

[4]伯格，H K.程序驗證和規(guī)范的形成方法[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