日本一道本高清一区二区-色妞熟女午夜福利在线视频-欧美成人情激情免费看-老司机午夜精品免费视频

近日，中國科學(xué)院軟件研究所科研人員針對信息物理融合系統(tǒng)的形式化建模和驗證，提出了基于擴(kuò)展體系結(jié)構(gòu)分析與設(shè)計語言的建模與驗證方法，為高速列車、車聯(lián)網(wǎng)等安全攸關(guān)系統(tǒng)的設(shè)計與驗證提供了新思路。安全攸關(guān)信息物理融合系統(tǒng)是復(fù)雜的嵌入式系統(tǒng)。傳統(tǒng)的建模方法往往難以同時兼顧軟件功能、物理環(huán)境和系統(tǒng)架構(gòu)三個維度，導(dǎo)致系統(tǒng)設(shè)計存在潛在風(fēng)險。在眾多架構(gòu)型建模語言中，體系結(jié)構(gòu)分析與設(shè)計語言表現(xiàn)得最為出色。然而，體系結(jié)構(gòu)分析與設(shè)計語言擅長描述系統(tǒng)架構(gòu)和硬件平臺，卻難以準(zhǔn)確描述系統(tǒng)的軟件功能和物理環(huán)境。該研究為實現(xiàn)信息物理融合系統(tǒng)“物理-軟件-硬件”三層架構(gòu)的統(tǒng)一建模，擴(kuò)展了應(yīng)用于實時嵌入式系統(tǒng)的體系結(jié)構(gòu)分析與設(shè)計語言，設(shè)計了Hybrid Annex附件，使體系結(jié)構(gòu)分析與設(shè)計語言能夠準(zhǔn)確描述離散的軟件功能、連續(xù)的物理變化及二者的交互過程；建立了從擴(kuò)展體系結(jié)構(gòu)分析與設(shè)計語言模型到形式化模型混成通信順序進(jìn)程的自動轉(zhuǎn)換框架，支持在形式模型層面對信息物理融合系統(tǒng)進(jìn)行仿真與驗證。進(jìn)一步，該研究采用擴(kuò)展的體系結(jié)構(gòu)分析與設(shè)計語言為一個汽車自動巡航系統(tǒng)建模，通過構(gòu)建包含物理行為層、軟件功能層和硬件平臺層的三層模型，可實現(xiàn)系統(tǒng)行為的仿真和驗證。實驗表明，該方法能夠有效觀察不同總線配置下的系統(tǒng)行為差異，為系統(tǒng)優(yōu)化提供依據(jù)。同時，研究還利用基于混成霍爾邏輯的定理證明工具，驗證了系統(tǒng)中緊急控制組件的安全性。相關(guān)研究成果發(fā)表在ACM TOSEM上。論文鏈接汽車自動巡航控制系統(tǒng)的擴(kuò)展體系結(jié)構(gòu)分析與設(shè)計語言架構(gòu)圖汽車在不同總線配置下的行車差異對比