基于前后断言法的温度控制系统程序验证
文章利用前后断言法对温度控制系统的设计进行验证，结论表明，该方法可以保證温度控制系统设计的正确性，保证系统可靠运行。
关键词：温度控制系统;程序验证;前后断言
随着物联网技术的发展，监控系统在工农业等多个领域，能够实现对环境的监测与控制功能。温度作为环境信息中最普遍的一个指标，在控制系统中常常作为主要的控制参数使用。温度控制系统[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<T1∧Con=-1。
对于通路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∧（Y<T1∧Con=-1 or Y>T2∧Con=1 or T1≤Y≤T2∧Con=0）X1=25∧X2=35∧T1=25∧T2=35∧Y=Tem∧（Y<T1∧Con=-1 or Y>T2∧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分别由Y<T1成立则Con=-1，由Y>T2则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