[發(fā)明專利]一種面向周期控制器的以模式為基礎(chǔ)的信物融合系統(tǒng)建模及驗(yàn)證方法

有效

• 申請(qǐng)?zhí)枺?/td>: 202110607529.X
• 申請(qǐng)日: 2021-06-01
• 公開（公告）號(hào): CN113434116B
• 公開（公告）日: 2022-09-20
• 發(fā)明（設(shè)計(jì)）人: 趙涌鑫;胡指銘;蒲戈光;劉虹
• 申請(qǐng)（專利權(quán)）人: 華東師范大學(xué);上海工業(yè)控制安全創(chuàng)新科技有限公司
• 主分類號(hào): G06F8/10
• 分類號(hào): G06F8/10;G06F8/35;G06F11/36
• 代理公司: 上海德禾翰通律師事務(wù)所 31319
• 代理人: 夏思秋

本發(fā)明公開了一種面向周期控制器的以模式為基礎(chǔ)的信物融合系統(tǒng)建模及驗(yàn)證方法，所述方法包括：利用信物融合系統(tǒng)建模語言，分別構(gòu)建抽象層面上的離散模式和連續(xù)模式，及具體層面上的離散控制流和連續(xù)控制流；結(jié)合上述獲得的抽象層面和具體層面的建模模型，獲得完整的信物融合系統(tǒng)模型，并以圖形化方式表示；將上述獲得的完整的信物融合系統(tǒng)模型中的變量、離散模式、連續(xù)模式、離散模式控制流、連續(xù)模式控制流按照翻譯規(guī)則轉(zhuǎn)換成混合自動(dòng)機(jī)，進(jìn)行形式化驗(yàn)證和性質(zhì)分析。本發(fā)明方法能以圖形化展示界面，方便用戶的理解和建立模型，也為模型和高置信的形式化性質(zhì)驗(yàn)證工具間建立有效的橋梁，節(jié)約信物融合系統(tǒng)模型的開發(fā)和高置信性質(zhì)驗(yàn)證的時(shí)間和成本。

技術(shù)領(lǐng)域

本發(fā)明屬于可信軟件、智慧城市和航空航天技術(shù)領(lǐng)域，涉及一種面向周期控制器的以模式為基礎(chǔ)的信物融合系統(tǒng)建模及驗(yàn)證方法。

背景技術(shù)

信物融合系統(tǒng)是由連續(xù)動(dòng)力學(xué)和離散動(dòng)力學(xué)組成的動(dòng)態(tài)系統(tǒng)，連續(xù)部分通常對(duì)物理環(huán)境的相互作用進(jìn)行建模，離散部分通常對(duì)控制系統(tǒng)的運(yùn)行進(jìn)行建模。計(jì)算和控制的結(jié)合可以導(dǎo)致非常復(fù)雜的系統(tǒng)設(shè)計(jì)，因此它們經(jīng)常出現(xiàn)在航空航天、汽車工業(yè)和工廠自動(dòng)化設(shè)計(jì)等領(lǐng)域。在航空航天領(lǐng)域，嵌入式軟件及其運(yùn)行環(huán)境具有高復(fù)雜性、不確定性和高實(shí)時(shí)性要求的特點(diǎn)。這就要求建模語言必須能夠描述系統(tǒng)和環(huán)境的不同組成部分，能夠深入刻畫嵌入式軟件的模型特征，能夠組合表達(dá)多種交互模式。航天器的控制器一般設(shè)計(jì)成周期模塊，對(duì)物理環(huán)境的進(jìn)化進(jìn)行監(jiān)控，并對(duì)時(shí)間具有較強(qiáng)的敏感性。由于這種周期控制器的計(jì)算和控制組合較為復(fù)雜，對(duì)系統(tǒng)設(shè)計(jì)的安全性要求也很高，因此如何對(duì)其建模并進(jìn)行形式化分析仍然是一個(gè)巨大的挑戰(zhàn)。

發(fā)明內(nèi)容

為了解決現(xiàn)有技術(shù)存在的不足，本發(fā)明的目的是提供一種面向周期控制器的以模式為基礎(chǔ)的信物融合系統(tǒng)建模及驗(yàn)證方法，以對(duì)信物融合系統(tǒng)進(jìn)行建模并進(jìn)行高置信的形式化分析。本發(fā)明提出的信物融合系統(tǒng)建模方法可以在模式層對(duì)信物融合系統(tǒng)進(jìn)行抽象層面的建模，抽象地表示控制器和物理環(huán)境以及他們間的交互轉(zhuǎn)移關(guān)系，將復(fù)雜的系統(tǒng)交互模式宏觀地表達(dá)出來，使得工程師能夠高效地理解和分析系統(tǒng)需求并建模，以便發(fā)現(xiàn)需求中是否存在不一致或不明確的地方；其次，每個(gè)離散模式都包含離散控制流來構(gòu)建控制器具體的控制邏輯，每個(gè)連續(xù)模式都包含連續(xù)控制流來構(gòu)建環(huán)境具體的物理變化規(guī)律。抽象和具體層面建模的結(jié)合構(gòu)成了完整的信物融合系統(tǒng)建模，并容易以圖形化的方式表示出來。本發(fā)明將信物融合系統(tǒng)建模模型轉(zhuǎn)換成混合自動(dòng)機(jī)的方法，提供了連接HHML和信物融合系統(tǒng)高置信的驗(yàn)證工具的橋梁，在此基礎(chǔ)上可以進(jìn)行相關(guān)高置信的形式化驗(yàn)證和性質(zhì)分析。

本發(fā)明提供了一種面向周期控制器的以模式為基礎(chǔ)的信物融合系統(tǒng)建模及驗(yàn)證方法，所述方法包括以下步驟：

步驟一、利用信物融合系統(tǒng)建模語言HHML，分別構(gòu)建抽象層面上表示控制器及交互轉(zhuǎn)移關(guān)系的離散模式和表示物理環(huán)境及交互轉(zhuǎn)移關(guān)系的連續(xù)模式；

步驟二、利用信物融合系統(tǒng)建模語言HHML，分別構(gòu)建具體層面上表示控制邏輯的離散控制流和表示物理變化規(guī)律的連續(xù)控制流；

步驟三、結(jié)合步驟一中獲得的抽象層面的建模模型和步驟二中獲得的具體層面的建模模型，獲得完整的信物融合系統(tǒng)模型，并以圖形化方式表示；

步驟四、將步驟三中獲得的完整的信物融合系統(tǒng)模型中的變量、離散模式、連續(xù)模式、離散模式控制流、連續(xù)模式控制流按照翻譯規(guī)則轉(zhuǎn)換成混合自動(dòng)機(jī)，進(jìn)行相關(guān)高置信的形式化驗(yàn)證和性質(zhì)分析。

步驟一中，所述抽象層面的建模在模式層進(jìn)行，抽象層面的建模可以抽象地表示控制器和物理環(huán)境以及他們之間的交互轉(zhuǎn)移關(guān)系，將復(fù)雜的系統(tǒng)交互模式宏觀地表達(dá)出來；所述模式層是指抽象層面的信物融合系統(tǒng)，包含離散模式和連續(xù)模式；所述離散模式是指抽象層面的控制器及轉(zhuǎn)移關(guān)系；所述連續(xù)模式是指抽象層面的物理環(huán)境及其轉(zhuǎn)移關(guān)系。