不確定環(huán)境下的人機(jī)物融合系統(tǒng)的建模與驗(yàn)證

發(fā)布時(shí)間：2020-10-30 02:18

　　隨著科技的進(jìn)步,新型復(fù)雜系統(tǒng)例如人機(jī)物融合系統(tǒng)(Human Cyber-Physical Systems,HCPS)已經(jīng)與人類社會生活越來越密不可分。軟件系統(tǒng)所處的信息空間與人們?nèi)粘Ｉ钏幍奈锢砜臻g日漸融合。物理空間內(nèi)環(huán)境的復(fù)雜多變、時(shí)空數(shù)據(jù)的爆發(fā)增長以及難以預(yù)料的人類行為等不確定因素威脅著系統(tǒng)安全。由于系統(tǒng)安全需求的增長,系統(tǒng)的規(guī)模和復(fù)雜度?隨之增加,所帶來的的一系列問題亟待解決。因此,在不確定環(huán)境下,構(gòu)造智能、安全的人機(jī)物融合系統(tǒng)的建模與驗(yàn)證方法以及工具鏈平臺的開發(fā)已經(jīng)成為軟件行業(yè)不可回避的挑戰(zhàn)。環(huán)境不確定性使得人機(jī)物融合系統(tǒng)軟件無法準(zhǔn)確感知其所處的運(yùn)行環(huán)境。感知的不確定性將導(dǎo)致系統(tǒng)的誤判,從而影響系統(tǒng)的安全性。環(huán)境不確定性使得系統(tǒng)設(shè)計(jì)人員無法為人機(jī)物融合系統(tǒng)軟件的運(yùn)行環(huán)境提供準(zhǔn)確的形式化規(guī)約。而對于安全要求較高的系統(tǒng),準(zhǔn)確的形式化規(guī)約是保證系統(tǒng)安全的首要條件。為了應(yīng)對規(guī)約的不確定性,本文提出時(shí)空數(shù)據(jù)驅(qū)動與模型驅(qū)動相結(jié)合的建模方式,即通過使用機(jī)器學(xué)習(xí)算法,基于環(huán)境中時(shí)空數(shù)據(jù),而非基于形式化規(guī)約,對環(huán)境進(jìn)行建模。根據(jù)安全軟件的典型特征,設(shè)計(jì)具有層次化特征的參數(shù)化建模語言,采用動態(tài)驗(yàn)證的方式保證系統(tǒng)的安全,從而構(gòu)建統(tǒng)一安全的理論框架。本文以構(gòu)建安全智能的人機(jī)物融合系統(tǒng)的形式化建模與驗(yàn)證的理論框架及應(yīng)用作為主要的研究目標(biāo)。主要貢獻(xiàn)體現(xiàn)在:·針對系統(tǒng)所處的物理環(huán)境的不確定性,應(yīng)用機(jī)器學(xué)習(xí)技術(shù),以環(huán)境中的時(shí)空數(shù)據(jù)為驅(qū)動,提出了不確定環(huán)境下的感知模型。包括基于樸素貝葉斯的人類行為分類模型和基于LSTM循環(huán)神經(jīng)網(wǎng)絡(luò)的環(huán)境風(fēng)險(xiǎn)預(yù)測模型�！ざx了具有層次化特征的參數(shù)化建模語言stohChart(p),給出了相應(yīng)語法和語義的形式化定義。提出了將模型轉(zhuǎn)換為隨機(jī)混成自動機(jī)(Stochastic Hybrid Automaton,SHA)的映射算法。·提出針對不確定性模型的動態(tài)驗(yàn)證方法,通過驗(yàn)證工具UPPAAL-SMC實(shí)現(xiàn)對模型的動態(tài)驗(yàn)證,從而定量評估不確定性環(huán)境以及人的行為對系統(tǒng)安全性的影響。為了展示方案的可行性,本文以自動駕駛車輛與人類駕駛車輛的交互場景為例說明了在不確定性環(huán)境下的人機(jī)物融合系統(tǒng)的建模與驗(yàn)證的具體應(yīng)用。
【學(xué)位單位】：華東師范大學(xué)
【學(xué)位級別】：博士
【學(xué)位年份】：2020
【中圖分類】：TP311.52
【部分圖文】：

框架圖,框架圖,技術(shù),環(huán)境

本文采用時(shí)空數(shù)據(jù)驅(qū)動的方法來處理環(huán)境的不確定性針對安全攸關(guān)HCPS建模與驗(yàn)證缺乏統(tǒng)一系統(tǒng)的理論、方法。圍繞“不確定環(huán)境下的人機(jī)物融合系統(tǒng)的建模與驗(yàn)證”關(guān)鍵科學(xué)問題,提出了以數(shù)據(jù)驅(qū)動和模型驅(qū)動相結(jié)合的創(chuàng)新方式構(gòu)建不確定環(huán)境下的HCPS,并對其關(guān)鍵支撐技術(shù)進(jìn)行創(chuàng)新性研究,圖1.1概述了本文所應(yīng)用的技術(shù)總框架圖,并且給出了對應(yīng)本文的行文結(jié)構(gòu)。?針對系統(tǒng)所處的物理環(huán)境的不確定性,應(yīng)用機(jī)器學(xué)習(xí)技術(shù),以環(huán)境中的時(shí)空數(shù)據(jù)為驅(qū)動,環(huán)境感知計(jì)算為切入點(diǎn),提出了不確定環(huán)境下的感知模型。包括基于樸素貝葉斯的人類行為分類模型和基于LSTM循環(huán)神經(jīng)網(wǎng)絡(luò)的環(huán)境風(fēng)險(xiǎn)預(yù)測模型。

神經(jīng)網(wǎng)絡(luò),貝葉斯,類別,概率

以上公式是樸素貝葉斯分類器的原理,即在給定n個特征的情況下,計(jì)算事件屬于某個類別的概率,概率最大的那個類別即為該事件所屬的類別。雖然原理很簡單,但卻有著驚人的學(xué)習(xí)效率和分類效果。原因之一就是我們不需要知道類別概率的精確值P(θ∈1,2,...,k),我們只需要分類器能夠?qū)λ鼈冞M(jìn)行正確的分類。樸素貝葉斯算法在機(jī)器學(xué)習(xí)中應(yīng)用非常廣泛,相比與其他監(jiān)督學(xué)習(xí)分類算法,它更簡單高效,需要考慮的參數(shù)也比較少。由于樸素貝葉斯可以很好地縮放到高維數(shù)據(jù),因此它經(jīng)常在多媒體應(yīng)用中被使用,特別是在文本處理中,已被證明分類效果十分準(zhǔn)確。樸素貝葉斯的算法主要包括三個階段:準(zhǔn)備階段,貝葉斯分類器學(xué)習(xí)階段以及預(yù)測階段。在準(zhǔn)備階段,需要進(jìn)行數(shù)據(jù)預(yù)處理,指定特征屬性和類別,獲取訓(xùn)練數(shù)據(jù)。進(jìn)入貝葉斯學(xué)習(xí)階段,首先要估計(jì)每個事件類別出現(xiàn)的概率,估計(jì)每個類別下每個特征屬性出現(xiàn)的概率,然后對于每個屬性組合,分別計(jì)算其歸屬于每個類別的概率。貝葉斯分類器學(xué)習(xí)階段完成,在預(yù)測階段,針對輸入的特征屬性集合,我們只需要挑選最大概率所屬的類別作為最終的分類結(jié)果。圖2.2長短時(shí)間記憶神經(jīng)網(wǎng)絡(luò)LSTM的神經(jīng)元結(jié)構(gòu)

神經(jīng)網(wǎng)絡(luò),神經(jīng)元