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

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

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

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

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

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

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

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

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

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

2? ? 基于前后斷言法的控制程序驗(yàn)證

2.1? 基本原理介紹

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

2.2? 程序驗(yàn)證過(guò)程

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

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

3? ? 程序模塊驗(yàn)證實(shí)例

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

3.1? 溫度控制實(shí)例說(shuō)明

以常見(jiàn)的溫度報(bào)警控制過(guò)程為例，說(shuō)明溫度控制主程序的執(zhí)行過(guò)程，流程圖如圖1所示。

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

3.2? 控制過(guò)程證明

圖1展示的過(guò)程中，在各個(gè)模塊下分別加以標(biāo)記從A到J，用以說(shuō)明問(wèn)題。不仿設(shè)本溫度監(jiān)控系統(tǒng)用于一個(gè)溫室監(jiān)測(cè)系統(tǒng)，因此，溫度范圍可以X1=25，X2=35;控制信息預(yù)置為0，代表溫度正常狀態(tài);傳感器讀取的溫度信息tem，臨時(shí)變量Y來(lái)存儲(chǔ)溫度信息。

證明這個(gè)程序的過(guò)程如下。

3.2.1? 建立斷言

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

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

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

3.2.2? 建立檢驗(yàn)條件

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

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

對(duì)于通路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

對(duì)于通路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。

對(duì)于通路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。

對(duì)于通路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? 驗(yàn)證檢驗(yàn)條件

對(duì)于通路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成立。

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

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

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

4? ? 結(jié)語(yǔ)

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

[參考文獻(xiàn)]

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

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

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

[4]伯格，H K.程序驗(yàn)證和規(guī)范的形成方法[M].北京：科學(xué)出版社，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