本文選題：信息-物理融合系統(tǒng) + 統(tǒng)計(jì)模型檢測　； 參考：《軟件學(xué)報》2017年05期

【摘要】：隨著計(jì)算機(jī)與物理環(huán)境的交互日益密切,信息-物理融合系統(tǒng)(cyber-physical system,簡稱CPS)在健康醫(yī)療、航空電子、智能建筑等領(lǐng)域具有廣泛的應(yīng)用前景,CPS的正確性、可靠性分析已引起人們的廣泛關(guān)注.統(tǒng)計(jì)模型檢測(statistical model checking,簡稱SMC)技術(shù)能夠?qū)PS進(jìn)行有效驗(yàn)證,并為系統(tǒng)的性能提供定量評估.然而,隨著系統(tǒng)規(guī)模的日益擴(kuò)大,如何提高統(tǒng)計(jì)模型檢測技術(shù)驗(yàn)證CPS的效率,是目前所面臨的主要困難之一.針對此問題,首先對現(xiàn)有SMC技術(shù)進(jìn)行實(shí)驗(yàn)分析,總結(jié)各種SMC技術(shù)的受限適用范圍和性能缺陷,并針對貝葉斯區(qū)間估計(jì)算法(Bayesian interval estimate,簡稱BIE)在實(shí)際概率接近0.5時需要大量路徑才能完成驗(yàn)證的缺陷,提出一種基于抽象和學(xué)習(xí)的統(tǒng)計(jì)模型檢測方法 AL-SMC.該方法采用主成分分析、前綴樹約減等技術(shù)對仿真路徑進(jìn)行學(xué)習(xí)和抽象,以減少樣本空間;然后,提出了一個面向CPS的自適應(yīng)SMC算法框架,可根據(jù)不同的概率區(qū)間自動選擇AL-SMC算法或者BIE算法,有效應(yīng)對不同情況下的驗(yàn)證問題;最后,結(jié)合經(jīng)典案例進(jìn)行實(shí)驗(yàn)分析,實(shí)驗(yàn)結(jié)果表明,自適應(yīng)SMC算法框架能夠在一定誤差范圍內(nèi)有效提高CPS統(tǒng)計(jì)模型檢測的效率,為CPS的分析驗(yàn)證提供了一種有效的途徑.
[Abstract]:With the increasingly close interaction between computer and physical environment, cyber-physical system (CPSfor short) has a wide application prospect in health care, avionics, intelligent building and so on. Reliability analysis has attracted wide attention. Statistical model checking (SMC) technology can effectively verify the performance of statistical model and provide quantitative evaluation for the performance of the system. However, with the increasing scale of the system, how to improve the efficiency of statistical model detection technology to verify CPS is one of the main difficulties. In order to solve this problem, the existing SMC technology is analyzed experimentally, and the limited application scope and performance defects of various SMC technologies are summarized. Aiming at the defects of Bayesian interval estimation (BIEs) algorithm, which requires a large number of paths to complete verification when the actual probability is close to 0.5, an abstract and learning-based statistical model detection method, AL-SMC-based, is proposed. In this method, principal component analysis and prefix tree reduction are used to study and abstract the simulation path to reduce the sample space. Then, an adaptive SMC algorithm framework for CPS is proposed. AL-SMC algorithm or BIE algorithm can be automatically selected according to different probabilistic intervals, which can effectively deal with the verification problem under different conditions. Finally, the experimental results show that, The adaptive SMC algorithm framework can effectively improve the efficiency of CPS statistical model detection within a certain error range, which provides an effective way for the analysis and verification of CPS.
【作者單位】： 教育部可信軟件國際合作聯(lián)合實(shí)驗(yàn)室(華東師范大學(xué));可信軟件國際聯(lián)合研究中心(華東師范大學(xué));上海市高可信重點(diǎn)實(shí)驗(yàn)室(華東師范大學(xué));
【基金】：國家自然科學(xué)基金(61472140,61170084) 上海市自然科學(xué)基金(14ZR1412500)~~
【分類號】：TP311

【參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 陳銘松;顧t，

本文編號：2036074