日立新技術(shù)，自動(dòng)驗(yàn)證汽車控制系統(tǒng)的安全要求

日立制作所與日立汽車系統(tǒng)公司2016年9月26日宣布共同開(kāi)發(fā)了一項(xiàng)新技術(shù)，該技術(shù)可針對(duì)設(shè)計(jì)開(kāi)發(fā)汽車控制系統(tǒng)時(shí)制定的安全要求，用計(jì)算機(jī)自動(dòng)驗(yàn)證這些要求是否存在遺漏。第三方測(cè)試認(rèn)證機(jī)構(gòu)——德國(guó)TUV SUD已確認(rèn)該技術(shù)可有效應(yīng)對(duì)功能安全標(biāo)準(zhǔn)ISO26262。

安全要求的定位。圖片來(lái)自日立

此次開(kāi)發(fā)的技術(shù)的要點(diǎn)。圖片來(lái)自日立

汽車控制系統(tǒng)開(kāi)發(fā)中的要求定義包括主功能（自動(dòng)駕駛系統(tǒng)等）相關(guān)要求，以及構(gòu)成主功能的控制系統(tǒng)發(fā)生故障時(shí)也能確保安全的安全要求。這些安全要求一直是使用英語(yǔ)和日語(yǔ)記述，但由于一句話或一個(gè)單詞有多種意思和解釋，表達(dá)經(jīng)常含糊不清，并不統(tǒng)一。而且，安全要求的記述還有可能發(fā)生遺漏，即便是專業(yè)技術(shù)人員，也要花費(fèi)大量時(shí)間進(jìn)行內(nèi)容確認(rèn)和驗(yàn)證。

此次的技術(shù)在記述安全要求時(shí)，運(yùn)用嚴(yán)密的數(shù)學(xué)性命題邏輯（推斷表達(dá)正確性的數(shù)學(xué)邏輯學(xué)之一）來(lái)定義，通過(guò)這種方法，使輸入到驗(yàn)證工具里的內(nèi)容更為明確。而且，還采用了能以簡(jiǎn)單的公式書(shū)寫(xiě)要求事項(xiàng)內(nèi)容的章法結(jié)構(gòu)，設(shè)計(jì)者可以輕松讀寫(xiě)。安全要求方面，針對(duì)希望系統(tǒng)具備的安全，將概略作為“上游要求”記述，將實(shí)現(xiàn)安全所需要的動(dòng)作及處理等詳細(xì)內(nèi)容作為“下流要求”記述。下游要求包括ECU（電子控制單元）、傳感器、致動(dòng)器、通信、軟件的構(gòu)成及處理，如果詳細(xì)記述，就會(huì)導(dǎo)致要求事項(xiàng)的數(shù)量增加。因此，驗(yàn)證工具會(huì)自動(dòng)驗(yàn)證上游要求和下游要求，并判斷是否存在遺漏。

另外，在相似系統(tǒng)之間或者同一系統(tǒng)內(nèi)的構(gòu)成部件之間，安全要求的記述內(nèi)容往往十分相似，因此，將已經(jīng)通過(guò)驗(yàn)證工具證明“沒(méi)有遺漏”的部分邏輯公式作為常見(jiàn)模式進(jìn)行再利用。比如，如果在相同條件下使用的傳感器B也需要進(jìn)行傳感器A那樣的異常檢測(cè)，便可將傳感器B的參數(shù)輸入傳感器A生成的模式中，由此自動(dòng)生成新要求事項(xiàng)的邏輯公式。通過(guò)對(duì)已驗(yàn)證模式進(jìn)行再利用，不僅可以防止新要求事項(xiàng)的遺漏，而且不需要增加新的書(shū)寫(xiě)內(nèi)容，可以提高作業(yè)效率。

據(jù)介紹，日立在電動(dòng)助力轉(zhuǎn)向器的控制系統(tǒng)中采用此次的技術(shù)，結(jié)果證實(shí)，可以記述和驗(yàn)證要求定義書(shū)中出現(xiàn)的所有安全要求事項(xiàng)。而且，與以前用英文記述時(shí)相比，記述量減少了30％，計(jì)算機(jī)自動(dòng)驗(yàn)證將用肉眼需要花費(fèi)約60分鐘的驗(yàn)證作業(yè)縮短到了約6分鐘。