[發(fā)明專利]用于軟件的自動(dòng)化誤差檢測(cè)和驗(yàn)證的方法

有效

• 申請(qǐng)?zhí)枺?/td>: 201110096514.8
• 申請(qǐng)日: 2011-04-18
• 公開(kāi)（公告）號(hào): CN102262586A
• 公開(kāi)（公告）日: 2011-11-30
• 發(fā)明（設(shè)計(jì)）人: D.巴特;D.V.奧格勒斯比;K.A.施勒格爾;G.馬德?tīng)?/a>
• 申請(qǐng)（專利權(quán)）人: 霍尼韋爾國(guó)際公司
• 主分類號(hào): G06F11/36
• 分類號(hào): G06F11/36
• 代理公司: 中國(guó)專利代理(香港)有限公司 72001
• 代理人: 王岳;蔣駿

相關(guān)申請(qǐng)的交叉引用

本申請(qǐng)要求2010年4月19日提交的美國(guó)臨時(shí)專利申請(qǐng)序號(hào)No.?61/325,804的權(quán)益，其通過(guò)引用結(jié)合到本文中。

技術(shù)領(lǐng)域

本發(fā)明涉及用于軟件的自動(dòng)化誤差檢測(cè)和驗(yàn)證的方法。

背景技術(shù)

飛行關(guān)鍵（flight-critical）軟件是包括傳感器和致動(dòng)器的飛機(jī)系統(tǒng)的一部分，并且將物理過(guò)程與計(jì)算相集成。此軟件控制許多不同的混合關(guān)鍵度（mixed-criticality）子系統(tǒng)并與之相交互，該子系統(tǒng)諸如引擎、制導(dǎo)和導(dǎo)航、燃料管理、飛行控制、通信、沖突檢測(cè)和解決、氣候控制以及娛樂(lè)。

軟件底層的算法是基于諸如代數(shù)學(xué)、分析、幾何學(xué)和三角學(xué)的數(shù)學(xué)原理。計(jì)算常常涉及由于所需計(jì)算的復(fù)雜性而未被正式工具充分地支持的非線性算術(shù)。通常，使用分立軟件系統(tǒng)來(lái)實(shí)現(xiàn)基于連續(xù)數(shù)學(xué)的模型。在此類模型中，用引入誤差（error）的浮點(diǎn)表示來(lái)近似數(shù)值。浮點(diǎn)計(jì)算可能同樣地引入誤差。另外，在由于抖動(dòng)、傳感器精度和外部機(jī)械或功能誤差而引入數(shù)值和定時(shí)誤差的分布式平臺(tái)上執(zhí)行軟件本身。

這些誤差可以累積，并且可以在質(zhì)量方面改變系統(tǒng)的行為（behavior）。任何時(shí)間，系統(tǒng)必須作出將兩個(gè)值（在一定程度上，那些值中的一者或兩者可能偏移了誤差）比較的判定（例如，如果-則-否則或循環(huán)結(jié)構(gòu)）。這可以促使系統(tǒng)執(zhí)行與在精確地表示值的情況下不同的行為。執(zhí)行在其周圍改變的值稱為“行為樞紐（pivot）值”。取決于行為樞紐值的判定能夠影響由軟件控制的系統(tǒng)的定時(shí)行為和物理性能。然而，當(dāng)前工具未將這些誤差考慮在內(nèi)，或者未可縮放到到足以支持工業(yè)級(jí)問(wèn)題。

發(fā)明內(nèi)容

提供了一種用于軟件的自動(dòng)化誤差檢測(cè)和驗(yàn)證的方法和系統(tǒng)。該方法包括提供軟件的模型，其中該模型包括一個(gè)或多個(gè)模型輸入和一個(gè)或多個(gè)模型輸出，以及被嵌入模型中的、每個(gè)具有相關(guān)區(qū)塊類型的多個(gè)區(qū)塊，所述區(qū)塊類型每個(gè)都具有多個(gè)相關(guān)區(qū)塊級(jí)（block-level）要求。所述方法還包括通過(guò)（across）所有區(qū)塊的計(jì)算語(yǔ)義學(xué)（computational?semantics）從模型輸入向模型輸出拓?fù)涞貍鞑ィ╬ropagate）一定范圍的信號(hào)值或變量值及誤差界（error?bound）。識(shí)別用于給定區(qū)塊的每個(gè)行為樞紐值并進(jìn)行檢驗(yàn)以確定以該誤差界來(lái)修改或擴(kuò)展傳播范圍是否將或可能促使信號(hào)值落在行為樞紐值的任一側(cè)。報(bào)告將或可能落在行為樞紐值的任一側(cè)的信號(hào)值的所有出現(xiàn)（occurrence）。

附圖說(shuō)明

參考附圖通過(guò)以下說(shuō)明，本發(fā)明的特征將變得對(duì)于本領(lǐng)域的技術(shù)人員來(lái)說(shuō)顯而易見(jiàn)。應(yīng)理解的是附圖僅描繪典型實(shí)施例，并且因此不應(yīng)將其視為范圍方面的限制，將通過(guò)使用附圖以附加的特殊性和細(xì)節(jié)來(lái)描述本發(fā)明，在附圖中：?

圖1是示出根據(jù)一種方法的用于軟件的自動(dòng)驗(yàn)證的過(guò)程的一般概述的過(guò)程流程圖；以及?

圖2是示出用于軟件的自動(dòng)驗(yàn)證的過(guò)程步驟的更多細(xì)節(jié)的過(guò)程流程圖。

具體實(shí)施方式

在以下詳細(xì)說(shuō)明中，足夠詳細(xì)地描述實(shí)施例以使得本領(lǐng)域的技術(shù)人員能夠?qū)嵤┍景l(fā)明。應(yīng)理解的是在不脫離本發(fā)明的范圍的情況下可以利用其它實(shí)施例。因此，不應(yīng)以限制性意義理解以下詳細(xì)說(shuō)明。

本發(fā)明涉及一種用于軟件誤差的自動(dòng)檢測(cè)的方法和系統(tǒng)；軟件誤差特別是由以下的組合引起的缺陷：（i）被要求的系統(tǒng)行為影響和變換的操作范圍，（ii）行為樞紐值，以及（iii）數(shù)值誤差。本方法提供模型的符號(hào)分析，其基于對(duì)范圍算術(shù)（range?arithmetic）的擴(kuò)展將計(jì)算、控制和實(shí)時(shí)性質(zhì)組合在統(tǒng)一分析框架中。

本方法還利用基于模型的方法進(jìn)行軟件設(shè)計(jì)和結(jié)果代碼的驗(yàn)證。到本方法的輸入是（i）系統(tǒng)行為要求的模型，（ii）模型的計(jì)算元素的行為語(yǔ)義學(xué)，（iii）數(shù)據(jù)類型和平臺(tái)相關(guān)約束/特性，以及（iv）模型輸入處的正常和最大操作信號(hào)范圍。所述輸出是可能由于數(shù)值誤差而出現(xiàn)的潛在誤差的報(bào)告，所述數(shù)值誤差促使特定的信號(hào)值與行為樞紐值交叉（cross）。這導(dǎo)致行為樞紐值周圍的不確定的行為。

這種方法與基于模擬的驗(yàn)證相比提供優(yōu)良的結(jié)果質(zhì)量，并且與傳統(tǒng)模型檢查方法相比提供優(yōu)良的可縮放性。因此，本發(fā)明在使用基于模型的方法開(kāi)發(fā)的商用航空電子軟件的自動(dòng)可縮放驗(yàn)證中特別有用。特別地，本發(fā)明提供用于諸如飛行控制和引擎控制的復(fù)雜商用航空電子應(yīng)用的認(rèn)證的航空電子系統(tǒng)的自動(dòng)驗(yàn)證。通過(guò)利用本方法，在保持對(duì)復(fù)雜現(xiàn)實(shí)問(wèn)題的可縮放性的同時(shí)，與傳統(tǒng)分析和測(cè)試方法相比可以實(shí)現(xiàn)平均的認(rèn)證成本方面的顯著改善。