[發(fā)明專利]基于UPPAAL的實(shí)時(shí)嵌入式系統(tǒng)構(gòu)件間協(xié)同行為的驗(yàn)證方法

有效

• 申請(qǐng)?zhí)枺?/td>: 201110423095.4
• 申請(qǐng)日: 2011-12-16
• 公開(kāi)（公告）號(hào): CN102567163A
• 公開(kāi)（公告）日: 2012-07-11
• 發(fā)明（設(shè)計(jì)）人: 杜德慧;溫巖;馮曙光;包丹珠;徐亞祎;杜麗
• 申請(qǐng)（專利權(quán)）人: 華東師范大學(xué)
• 主分類號(hào): G06F11/26
• 分類號(hào): G06F11/26
• 代理公司: 上海藍(lán)迪專利事務(wù)所 31215
• 代理人: 徐筱梅;張翔

1.一種基于UPPAAL的實(shí)時(shí)嵌入式系統(tǒng)構(gòu)件間協(xié)同行為的驗(yàn)證方法，其特征在于該方法是：將實(shí)時(shí)嵌入式系統(tǒng)建模形成的MARTE模型轉(zhuǎn)化為工具UPPAAL能夠驗(yàn)證的時(shí)間自動(dòng)機(jī)，然后使用UPPAAL工具對(duì)時(shí)間自動(dòng)機(jī)驗(yàn)證，并得出驗(yàn)證結(jié)果；具體包括以下步驟：

a、實(shí)時(shí)嵌入式系統(tǒng)MARTE模型轉(zhuǎn)化為時(shí)間自動(dòng)機(jī)

ⅰ)、對(duì)于MARTE模型中有CCSL約束的MARTE構(gòu)件圖，根據(jù)CCSL語(yǔ)義將構(gòu)件模型轉(zhuǎn)化為仿真自動(dòng)機(jī)；?

ⅱ)、對(duì)于MARTE模型中沒(méi)有CCSL約束的MARTE構(gòu)件圖，首先，將模型中的MARTE順序圖轉(zhuǎn)化為監(jiān)控自動(dòng)機(jī)；然后，將模型中的MARTE狀態(tài)圖轉(zhuǎn)化為對(duì)象時(shí)間自動(dòng)機(jī)；?

b、使用工具UPPAAL對(duì)轉(zhuǎn)化好的時(shí)間自動(dòng)機(jī)模型進(jìn)行驗(yàn)證并輸出驗(yàn)證結(jié)果。

2.根據(jù)權(quán)利要求1所述的驗(yàn)證方法，其特征在于所述根據(jù)CCSL語(yǔ)義將構(gòu)件模型轉(zhuǎn)化為仿真自動(dòng)機(jī)是：根據(jù)各個(gè)端口CCSL語(yǔ)義，將構(gòu)件的每一個(gè)端口建模成一個(gè)從時(shí)間自動(dòng)機(jī)，各從時(shí)間自動(dòng)機(jī)負(fù)責(zé)模擬對(duì)應(yīng)端口的協(xié)同行為；同時(shí)將整個(gè)構(gòu)件建模為主時(shí)間自動(dòng)機(jī)，主時(shí)間自動(dòng)機(jī)通過(guò)同步機(jī)制控制各從自動(dòng)機(jī)的行為。

3.根據(jù)權(quán)利要求1所述的驗(yàn)證方法，其特征在于所述將模型中的MARTE順序圖轉(zhuǎn)化為監(jiān)控自動(dòng)機(jī)的過(guò)程是：模型驗(yàn)證是通過(guò)message的傳遞作為建模依據(jù)的；首先，將message作為一個(gè)監(jiān)控對(duì)象，根據(jù)每一個(gè)message的接收方和發(fā)送方，message的前后關(guān)系和message中所包含的時(shí)間約束對(duì)應(yīng)地生成UPPAAL監(jiān)控自動(dòng)機(jī)的狀態(tài)遷移和信號(hào)變量，然后再轉(zhuǎn)化為監(jiān)控自動(dòng)機(jī)，用來(lái)對(duì)整個(gè)系統(tǒng)的交互行為進(jìn)行監(jiān)控。

4.根據(jù)權(quán)利要求1所述的驗(yàn)證方法，其特征在于所述將模型中的MARTE狀態(tài)圖轉(zhuǎn)化為時(shí)間自動(dòng)機(jī)的過(guò)程是：MARTE狀態(tài)圖對(duì)應(yīng)地為一個(gè)系統(tǒng)構(gòu)件建模；構(gòu)件內(nèi)部的事件信息通過(guò)MARTE狀態(tài)圖表示；事件信息包括外部交互信息和內(nèi)部的更新信息；將MARTE狀態(tài)圖中的各狀態(tài)一一對(duì)應(yīng)地轉(zhuǎn)化為時(shí)間自動(dòng)機(jī)中的location，根據(jù)狀態(tài)之間的遷移相應(yīng)地轉(zhuǎn)化為時(shí)間自動(dòng)機(jī)中的edge，對(duì)于狀態(tài)圖中對(duì)其他對(duì)象的調(diào)用轉(zhuǎn)化為synchronization，將狀態(tài)圖內(nèi)部變量更新轉(zhuǎn)化為effect，狀態(tài)圖中控制變量轉(zhuǎn)化為guard；最后再在涉及到交互的edge中加入額外的synchronization和effect，以便監(jiān)控自動(dòng)機(jī)收集信號(hào)。