同濟(jì)大學(xué)軟件學(xué)院 楊 嘯

1.引言

隨著嵌入式系統(tǒng)的廣泛應(yīng)用，產(chǎn)品的功能安全性已成為設(shè)計(jì)的重點(diǎn)問題之一，尤其在汽車領(lǐng)域。目前電子工業(yè)中最普遍的功能安全標(biāo)準(zhǔn)是IEC 61508[1]。

IEC 61508提出功能安全的概念，功能安全作為安全性的一部分，取決于系統(tǒng)或設(shè)備正確地響應(yīng)其輸入。功能安全性的保障是通過對(duì)潛在危險(xiǎn)情況進(jìn)行檢測，并采取相應(yīng)的安全措施或機(jī)制，來防止危害性事件發(fā)生或緩解其造成的危害。因此，監(jiān)測產(chǎn)品是否發(fā)生故障對(duì)保證功能安全有重要意義。

在嵌入式環(huán)境的實(shí)時(shí)監(jiān)測已有相關(guān)的研究，Donal Heffernan和Ciaran MacNamee將實(shí)時(shí)驗(yàn)證擴(kuò)展到功能安全性的驗(yàn)證[2]。在他們的工作中，設(shè)計(jì)了硬件電路用于監(jiān)測控制網(wǎng)（CAN）的消息，以實(shí)時(shí)驗(yàn)證安全性。，然而通過CAN總線無法監(jiān)測軟件內(nèi)部變量，因此無法驗(yàn)證嵌入式應(yīng)用本身是否發(fā)生故障。

本文旨在對(duì)嵌入式產(chǎn)品提供故障實(shí)時(shí)檢測方案。設(shè)計(jì)了一個(gè)FPGA硬件模塊，通過SPI（Serial Peripheral Interface）總線，在嵌入式產(chǎn)品運(yùn)行階段獲取需要監(jiān)測的變量信息，并根據(jù)FPGA內(nèi)設(shè)計(jì)的驗(yàn)證模塊檢測故障是否發(fā)生。

2.故障實(shí)時(shí)檢測系統(tǒng)簡介

2.1 線性時(shí)態(tài)邏輯

Amir Pnueli[3]定義了線性時(shí)間邏輯（LTL），它為復(fù)雜系統(tǒng)的簡化提供了強(qiáng)大的形式化體系。文獻(xiàn)[4]使用LTL表達(dá)故障，并將其用于模型檢驗(yàn)。

例如一個(gè)圖像識(shí)別應(yīng)用的故障是攝像頭未啟動(dòng)或捕獲圖像超時(shí)或檢測時(shí)間超時(shí)。用LTL公式表達(dá)如下：

2.2 實(shí)時(shí)檢測模塊架構(gòu)

為了能夠在運(yùn)行階段檢測應(yīng)用的行為，監(jiān)控模塊需要獲得相關(guān)的變量，被檢測應(yīng)用通過SPI總線將變量信息傳輸?shù)奖O(jiān)控模塊。在研究中，假設(shè)傳輸是無誤的并且足夠快，以使驗(yàn)證能夠?qū)崟r(shí)地進(jìn)行。

本設(shè)計(jì)使用Xilinx ZYNQ全可編程片上系統(tǒng)（All Programmable Systems on Chips, APSoCs）以軟硬件協(xié)同的設(shè)計(jì)方法實(shí)現(xiàn)故障檢測系統(tǒng)。系統(tǒng)主要包括五個(gè)功能模塊：數(shù)據(jù)通信、數(shù)據(jù)解析、AP評(píng)估、公式驗(yàn)證和計(jì)時(shí)器。其中AP評(píng)估和公式驗(yàn)證使用FPGA實(shí)現(xiàn)，以保證結(jié)果輸出的實(shí)時(shí)性，另外對(duì)于計(jì)時(shí)器，也使用FPGA硬件電路實(shí)現(xiàn)，以獲得真實(shí)的物理時(shí)間。數(shù)據(jù)通信使用FPGA實(shí)現(xiàn)SPI從機(jī)接收功能，將接收到的數(shù)據(jù)存放在寄存器中，然后由軟件部分讀取并進(jìn)行解析，獲得所需變量的值。

系統(tǒng)整體架構(gòu)如圖1所示，ZYNQ分為PL和PS兩部分，PL是可編程邏輯（Programmable Logic），由FPGA硬件電路實(shí)現(xiàn)；PS即處理器系統(tǒng)（Processing System），運(yùn)行于ARM處理器。

圖1 硬件監(jiān)控模塊架構(gòu)框圖

在接收到全局變量所需的值后，AP評(píng)估模塊故障表達(dá)式的每個(gè)基本事件進(jìn)行評(píng)估。故障表達(dá)式的最終結(jié)果在公式驗(yàn)證模塊中實(shí)時(shí)評(píng)估，以檢測故障是否發(fā)生。為了評(píng)估與時(shí)間有關(guān)的原子命題，在電路中設(shè)計(jì)了一個(gè)獨(dú)立的時(shí)鐘。外部接口用于向用戶顯示結(jié)果，或?qū)⒔Y(jié)果發(fā)送給其他應(yīng)用程序以實(shí)現(xiàn)安全性控制。

3.測試與結(jié)果分析

3.1 實(shí)驗(yàn)方案

評(píng)估環(huán)境配置如圖2所示。實(shí)時(shí)檢測系統(tǒng)運(yùn)行于ZYNQ，嵌入式應(yīng)用通過SPI連接，并將檢測結(jié)果顯示在用戶界面（PC）。

在實(shí)驗(yàn)中，通過在嵌入式應(yīng)用運(yùn)行期間注入故障，實(shí)時(shí)檢測模塊能夠及時(shí)輸出檢測結(jié)果，并顯示檢測用時(shí)。根據(jù)檢測結(jié)果和用時(shí)驗(yàn)證實(shí)時(shí)檢測系統(tǒng)的有效性。

圖2 實(shí)驗(yàn)評(píng)估環(huán)境

3.2 實(shí)驗(yàn)結(jié)果分析

本實(shí)驗(yàn)使用前文提到的故障示例進(jìn)行測試，測試結(jié)果如表1所示。其中第四項(xiàng)故障，由于并未設(shè)計(jì)在實(shí)時(shí)檢測模塊內(nèi)，因此未檢測到違反。檢測結(jié)果表名實(shí)時(shí)檢測系統(tǒng)能夠在應(yīng)用運(yùn)行期間正確地檢測到故障發(fā)生。

檢測用時(shí)如表2所示。以視頻常用幀率30fps，則圖像采集周期為30ms，而故障檢測用時(shí)遠(yuǎn)小于這一周期，可見FPGA具有良好的實(shí)時(shí)性。

表1 功能測試結(jié)果

表2 實(shí)時(shí)性測試結(jié)果（ms）

4.結(jié)束語

為了保證嵌入式產(chǎn)品的安全性，產(chǎn)品故障必須及時(shí)發(fā)現(xiàn)，否則當(dāng)系統(tǒng)失效或事故發(fā)生，無法及時(shí)采取安全措施，或已經(jīng)對(duì)環(huán)境和人員造成損害。

本文設(shè)計(jì)一個(gè)獨(dú)立的實(shí)時(shí)檢測系統(tǒng)模塊，在軟件的運(yùn)行階段，實(shí)時(shí)接收軟件變量信息，并根據(jù)故障表達(dá)式判斷故障是否發(fā)生。故障注入的測試表明，實(shí)時(shí)檢測系統(tǒng)在軟件發(fā)生故障時(shí)，能夠準(zhǔn)確和及時(shí)給出檢測結(jié)果。

本文的研究工作設(shè)計(jì)了故障實(shí)時(shí)檢測的原型系統(tǒng)，證明了在軟件運(yùn)行階段檢測故障的合理性，為保證產(chǎn)品安全提供有效依據(jù)。

[1]靳江紅,吳宗之,胡玢.對(duì)功能安全基礎(chǔ)標(biāo)準(zhǔn)IEC61508的研究[J].中國安全生產(chǎn)科學(xué)技術(shù),2009,5(02):71-75.

[2]D.Heffernan,C.MacNamee,Runtime observation of functional safety properties in an automotive control network[J].Journal of Systems Architecture 68(2016):38–50.

[3]A.Pnueli,The temporal logic of programs,in:Foundations of Computer Science,1977,18th Annual Symposium on,IEEE,1977, pp.46–57.

[4]馬琳. 基于故障樹的航電軟件系統(tǒng)安全性驗(yàn)證方法研究[D].南京航空航天大學(xué),2012.