武 鵬，吳盡昭，2，3，4*

（1.北京交通大學(xué)計(jì)算機(jī)與信息技術(shù)學(xué)院，北京 100044；2.中國(guó)科學(xué)院成都計(jì)算機(jī)應(yīng)用研究所，成都 610041；3.廣西大學(xué)計(jì)算機(jī)與電子信息學(xué)院，南寧 530004；4.廣西民族大學(xué)人工智能學(xué)院，南寧 530006）

0 引言

形式化驗(yàn)證屬于形式化方法的范疇，形式化驗(yàn)證主要包含兩種方法，模型檢驗(yàn)和定理證明。模型檢測(cè)是由Clarke和Emerson提出的，主要通過(guò)搜索系統(tǒng)狀態(tài)空間來(lái)驗(yàn)證系統(tǒng)的正確性的一種方法［1］。而定理證明主要解決如何利用邏輯和數(shù)學(xué)推理證明的手段驗(yàn)證軟件的關(guān)鍵性質(zhì)。這兩種方法優(yōu)勢(shì)互補(bǔ)，在學(xué)術(shù)界［2-3］、工業(yè)界［4］得到了廣泛應(yīng)用。定理證明中的推理方法是演繹推理范疇，其中語(yǔ)法、語(yǔ)義、推理規(guī)則涉及其中，許多學(xué)者在這一領(lǐng)域有廣泛的深入研究［5-6］。標(biāo)簽變遷系統(tǒng)或其相似結(jié)構(gòu)廣泛應(yīng)用在模型檢驗(yàn)和定理證明相關(guān)的驗(yàn)證領(lǐng)域，它是刻畫(huà)系統(tǒng)的變遷行為的常用技術(shù)手段［7］。其中，系統(tǒng)各個(gè)狀態(tài)及變遷條件通過(guò)相應(yīng)邏輯賦值及其滿足的條件來(lái)刻畫(huà)。然而，二值或多值邏輯在描述復(fù)雜系統(tǒng)的狀態(tài)并不完全有效［8］。實(shí)多項(xiàng)式代數(shù)變遷系統(tǒng)將二值邏輯和多值邏輯的狀態(tài)空間擴(kuò)展到Rn域，這在描述復(fù)雜系統(tǒng)行為和驗(yàn)證復(fù)雜系統(tǒng)安全性質(zhì)上更有效［9］。近年來(lái)，在混成系統(tǒng)的驗(yàn)證領(lǐng)域，微分多項(xiàng)式代數(shù)和不變量理論［10-11］相繼被提出，這進(jìn)一步地拓寬了基于定理證明的推理方法的應(yīng)用領(lǐng)域。

另一方面，在復(fù)雜系統(tǒng)中，系統(tǒng)參數(shù)有時(shí)并不是精確確定的，大多數(shù)情況下只知道這些參數(shù)的取值范圍，這增加了這些系統(tǒng)的推理驗(yàn)證工作的難度。例如，許多基于多項(xiàng)式的定理證明系統(tǒng)中廣泛運(yùn)用了Grobner基方法，然而多項(xiàng)式方程組的Grobner基對(duì)系數(shù)是不連續(xù)的［12］，這大大增加了推理驗(yàn)證方法處理誤差參數(shù)多項(xiàng)式系統(tǒng)的難度。而系統(tǒng)的誤差又是普遍存在的。工程上，在驗(yàn)證系統(tǒng)某些性質(zhì)的過(guò)程中，對(duì)變遷條件的刻畫(huà)是確定的數(shù)值，而這恰恰是工程上無(wú)法做到的。例如，當(dāng)系統(tǒng)溫度等于90°時(shí)，停止供熱。但實(shí)際中，無(wú)法精確測(cè)量溫度剛好到達(dá)90°，測(cè)量的過(guò)程都伴隨著一定的誤差。在系統(tǒng)變遷的過(guò)程中，往往有若干個(gè)閾值條件來(lái)觸發(fā)系統(tǒng)的變遷，這就需要對(duì)這若干個(gè)系統(tǒng)參數(shù)精確測(cè)量。而事實(shí)上，這是不可能做到的，測(cè)量的過(guò)程總是伴隨著一定的誤差。多個(gè)誤差變量的累計(jì)和傳遞過(guò)程中，系統(tǒng)可能出現(xiàn)錯(cuò)誤的變遷行為。是否能定量地將誤差參數(shù)結(jié)合到推理方法中，并應(yīng)用于含誤差參數(shù)系統(tǒng)的推理驗(yàn)證工作中？筆者在文獻(xiàn)［13］中給出了線性誤差斷言零點(diǎn)集的凸集性的證明，但未給出求線性誤差斷言所有頂點(diǎn)的方法和相關(guān)證明；而求取這些頂點(diǎn)是文本方法步驟的必不可少的環(huán)節(jié)，也是實(shí)現(xiàn)本文方法的難點(diǎn)。本文給出了求線性誤差斷言頂點(diǎn)的具體方法并證明了該方法的正確性，之后給出文本方法在驗(yàn)證火車(chē)加速狀態(tài)的應(yīng)用，求取了火車(chē)加速狀態(tài)的參數(shù)化頂點(diǎn)，將看似非線性問(wèn)題處理為線性問(wèn)題，進(jìn)一步擴(kuò)大了本文方法的應(yīng)用范圍。這在以往的文獻(xiàn)中是鮮有報(bào)道的。本文給出的推理方法可用于線性誤差系統(tǒng)的推理驗(yàn)證工作中。

1 誤差的區(qū)間數(shù)刻畫(huà)

誤差是普遍存在的，有時(shí)也是必不可免的。在推理方法中引入誤差，就需要對(duì)誤差做定量刻畫(huà)。誤差常常是限定的一個(gè)區(qū)域，而區(qū)間數(shù)是數(shù)的推廣，區(qū)間數(shù)在許多方面已經(jīng)成功應(yīng)用［14-16］，下面介紹區(qū)間數(shù)的運(yùn)算規(guī)則。

區(qū)間數(shù)是實(shí)數(shù)的推廣，當(dāng)a-=a+時(shí)，-a為實(shí)數(shù)。然而上述定義的區(qū)間數(shù)的四則運(yùn)算是不可逆的，下面給出例子。

若a為實(shí)數(shù)，則式（1）則一定成立。然而若a，b為區(qū)間數(shù)，式（1）不一定成立。

但這并不意味著包含上述四則運(yùn)算的推理過(guò)程是錯(cuò)誤的，只是推理過(guò)程不可逆，即推理的結(jié)論是前提的一個(gè)必要條件，而非充分必要條件。在包含誤差的推理的過(guò)程中，運(yùn)算次數(shù)的增多，可能會(huì)導(dǎo)致結(jié)果沒(méi)有實(shí)際意義，所以在推理過(guò)程中，要嘗試其他方法。本文的方法提供了一種思路。

2 線性誤差斷言及蘊(yùn)含關(guān)系

2.1 線性誤差斷言

2.2 蘊(yùn)含關(guān)系

蘊(yùn)含關(guān)系是基于定理證明的形式化驗(yàn)證領(lǐng)域重要環(huán)節(jié)，也是推理規(guī)則的基礎(chǔ)問(wèn)題。φ1蘊(yùn)含φ2表示：如果φ1為真，則φ2一定為真。記作φ1|=φ2。例如：φ1：x-1=0，φ2：x2-1=0，顯然有：φ1|=φ2。基于多項(xiàng)式斷言的蘊(yùn)含關(guān)系［17］中有這樣一個(gè)充要條件：φ1|=φ2的充分必要條件為Zero(φ1)?Zero(φ2)。這同樣適用于線性誤差斷言。下面給出線性誤差斷言的蘊(yùn)含關(guān)系的充分必要條件。

3 推理方法

4 實(shí)例分析

4.1 火車(chē)加速狀態(tài)分析

下面以火車(chē)加速運(yùn)動(dòng)為例分析。為了便于分析，假設(shè)火車(chē)有2個(gè)車(chē)廂（8車(chē)廂和16車(chē)廂問(wèn)題可由兩車(chē)廂問(wèn)題遞歸得到），兩車(chē)廂各有動(dòng)力輸出?；疖?chē)在加速過(guò)程中，當(dāng)————guard為v=80 m s=288km h滿足時(shí)，火車(chē)由加速狀態(tài)轉(zhuǎn)變?yōu)閯蛩贍顟B(tài)（由圖1所示），-φ、-?為加速狀態(tài)和勻速狀態(tài)各自正常工作滿足的條件。在火車(chē)的加速狀態(tài)中，如果-φ不滿足，則火車(chē)加速狀態(tài)異常，需立即檢測(cè)異常。

圖1 火車(chē)狀態(tài)變遷Fig.1 Train state transition

f1、f2分別表示車(chē)廂1與車(chē)廂2各自提供的牽引力。f12為車(chē)廂1對(duì)車(chē)廂2的作用力，為一區(qū)間數(shù)。m1、m2代表每個(gè)車(chē)廂的初始質(zhì)量。Δm1、Δm2代表車(chē)廂的質(zhì)量變化（由于乘客和行李的變化），為區(qū)間數(shù)。ζ是一個(gè)關(guān)聯(lián)空氣密度壓強(qiáng)的系數(shù)，由于風(fēng)、海拔等因素的變化，ζ為區(qū)間數(shù)。a表示加速度。g為重力加速度。

下面給出上述變量值，m1=50 000 kg，Δm1=[0，0.2m1]，m2=50 000 kg， Δm2=[0，0.2m2]，ζ=[1.5，1.6]kg m，μ=0.01，a=0.4 m s2，f12=[0，2 000]N，g=10 m s2。

由力學(xué)知識(shí)，可有式（20）：

由第3章的推理方法的步驟2得式（21）：

圖2 的空間區(qū)域Fig.2 Spatial region of Zero(-φ)

4.2 模擬與測(cè)試

將式（22）代入式（20），可得到n個(gè)解，表示如式（23）：

將式（23）中的n個(gè)解分別代入式（21），來(lái)驗(yàn)證是否滿足該不等式組。分別測(cè)試了n=1 000，n=10 000，n=100 000的情況。其中圖3和圖4為1 000個(gè)解的空間位置（n=1000）。圖5為10 000個(gè)解的空間位置（n=10 000）。圖6為100 000個(gè)解的空間位置（n=100 000）。

圖3 1 000個(gè)測(cè)試用例Fig.3 A thousand test cases

圖4 圖3的另一角度Fig.4 Another angleof Fig.3

圖5 10 000個(gè)測(cè)試用例Fig.5 Ten thousand test cases

圖6 100 000個(gè)測(cè)試用例Fig.6 Onehundred thousand test cases

經(jīng)測(cè)試，所有的解都在式（21）表示的區(qū)域內(nèi)。這個(gè)區(qū)域表示由不確定誤差系數(shù)導(dǎo)致的可能的動(dòng)力分配區(qū)域，以保證列車(chē)平穩(wěn)加速行駛。如果列車(chē)平穩(wěn)加速過(guò)程中的動(dòng)力分配不在這個(gè)區(qū)域內(nèi)部，或始終接近該區(qū)域的邊界時(shí)，則表示存在非誤差因素對(duì)動(dòng)力系統(tǒng)的影響。這時(shí)需要排除是否存在機(jī)械故障，比如車(chē)軸軸承或電機(jī)軸承是否需要更換潤(rùn)滑脂。

4.3 推理分析

其中t∈[0，200]。

5 結(jié)語(yǔ)

對(duì)于系數(shù)和變量有誤差的系統(tǒng)，大多數(shù)以前的推理方法都不適用。但是文獻(xiàn)［18］方法對(duì)具有單個(gè)誤差變量的多項(xiàng)式系統(tǒng)有非常高的理論價(jià)值。在多個(gè)誤差變量的推理方法上，已有的文獻(xiàn)還少有報(bào)道。另一方面，針對(duì)誤差的模糊推理［19］也有一些學(xué)者在研究，這類(lèi)方法最終給出了推理結(jié)論正確性的模糊程度或類(lèi)似結(jié)論，這與本文提出的推理方法是有區(qū)別的，本文的推理方法最終可以給出推理結(jié)論是否正確的確定性回答。

本文推理方法可對(duì)給定誤差區(qū)間的線性斷言進(jìn)行可靠的推理。此外，對(duì)于那些零點(diǎn)不完全非負(fù)的線性誤差斷言，可用變量替換將其零點(diǎn)全部做非負(fù)處理。例如，攝氏溫度c是有可能出現(xiàn)負(fù)值的，可以用一個(gè)變量替換c'=c+273.15，其中c'表示其相應(yīng)的開(kāi)爾文溫度（絕對(duì)溫度）。然而，在非線性誤差多項(xiàng)式斷言的推理方法上，目前仍沒(méi)有有效的解決方法。結(jié)合控制點(diǎn)生成方法，有望將非線性誤差多項(xiàng)式斷言的零點(diǎn)集作線性化包含處理，這樣可以進(jìn)一步擴(kuò)大該方法應(yīng)用范圍，這也是今后的工作方向。