不確定環(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)與人類社會(huì)生活越來越密不可分。軟件系統(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)證方法以及工具鏈平臺(tái)的開發(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ī)約。而對(duì)于安全要求較高的系統(tǒng),準(zhǔn)確的形式化規(guī)約是保證系統(tǒng)安全的首要條件。為了應(yīng)對(duì)規(guī)約的不確定性,本文提出時(shí)空數(shù)據(jù)驅(qū)動(dòng)與模型驅(qū)動(dòng)相結(jié)合的建模方式,即通過使用機(jī)器學(xué)習(xí)算法,基于環(huán)境中時(shí)空數(shù)據(jù),而非基于形式化規(guī)約,對(duì)環(huán)境進(jìn)行建模。根據(jù)安全軟件的典型特征,設(shè)計(jì)具有層次化特征的參數(shù)化建模語言,采用動(dòng)態(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)在:·針對(duì)系統(tǒng)所處的物理環(huán)境的不確定性,應(yīng)用機(jī)器學(xué)習(xí)技術(shù),以環(huán)境中的時(shí)空數(shù)據(jù)為驅(qū)動(dòng),提出了不確定環(huán)境下的感知模型。包括基于樸素貝葉斯的人類行為分類模型和基于LSTM循環(huán)神經(jīng)網(wǎng)絡(luò)的環(huán)境風(fēng)險(xiǎn)預(yù)測(cè)模型�！ざx了具有層次化特征的參數(shù)化建模語言stohChart(p),給出了相應(yīng)語法和語義的形式化定義。提出了將模型轉(zhuǎn)換為隨機(jī)混成自動(dòng)機(jī)(Stochastic Hybrid Automaton,SHA)的映射算法。·提出針對(duì)不確定性模型的動(dòng)態(tài)驗(yàn)證方法,通過驗(yàn)證工具UPPAAL-SMC實(shí)現(xiàn)對(duì)模型的動(dòng)態(tài)驗(yàn)證,從而定量評(píng)估不確定性環(huán)境以及人的行為對(duì)系統(tǒng)安全性的影響。為了展示方案的可行性,本文以自動(dòng)駕駛車輛與人類駕駛車輛的交互場(chǎng)景為例說明了在不確定性環(huán)境下的人機(jī)物融合系統(tǒng)的建模與驗(yàn)證的具體應(yīng)用。
【學(xué)位單位】：華東師范大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位年份】：2020
【中圖分類】：TP311.52
【部分圖文】：

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

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

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

以上公式是樸素貝葉斯分類器的原理,即在給定n個(gè)特征的情況下,計(jì)算事件屬于某個(gè)類別的概率,概率最大的那個(gè)類別即為該事件所屬的類別。雖然原理很簡單,但卻有著驚人的學(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)確。樸素貝葉斯的算法主要包括三個(gè)階段:準(zhǔn)備階段,貝葉斯分類器學(xué)習(xí)階段以及預(yù)測(cè)階段。在準(zhǔn)備階段,需要進(jìn)行數(shù)據(jù)預(yù)處理,指定特征屬性和類別,獲取訓(xùn)練數(shù)據(jù)。進(jìn)入貝葉斯學(xué)習(xí)階段,首先要估計(jì)每個(gè)事件類別出現(xiàn)的概率,估計(jì)每個(gè)類別下每個(gè)特征屬性出現(xiàn)的概率,然后對(duì)于每個(gè)屬性組合,分別計(jì)算其歸屬于每個(gè)類別的概率。貝葉斯分類器學(xué)習(xí)階段完成,在預(yù)測(cè)階段,針對(duì)輸入的特征屬性集合,我們只需要挑選最大概率所屬的類別作為最終的分類結(jié)果。圖2.2長短時(shí)間記憶神經(jīng)網(wǎng)絡(luò)LSTM的神經(jīng)元結(jié)構(gòu)

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