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

有效

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

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

本發(fā)明涉及模型構(gòu)件和驗(yàn)證技術(shù)領(lǐng)域，特別是一種基于UPPAAL的實(shí)時(shí)嵌入式系統(tǒng)構(gòu)件間協(xié)同行為的驗(yàn)證方法。

背景技術(shù)

實(shí)時(shí)嵌入式系統(tǒng)中，任何一點(diǎn)錯(cuò)誤都可能導(dǎo)致災(zāi)難的發(fā)生，因此保障安全性、可靠性是建立實(shí)時(shí)嵌入式系統(tǒng)的首要問題。對(duì)于傳統(tǒng)的實(shí)時(shí)嵌入式系統(tǒng)由于構(gòu)件總體設(shè)計(jì)、構(gòu)件交互行為和構(gòu)件狀態(tài)信息三者在設(shè)計(jì)時(shí)處于不同的建模階段和時(shí)期，因此，最后交付的模型中往往會(huì)存在不一致的現(xiàn)象，從而對(duì)今后系統(tǒng)的具體實(shí)現(xiàn)增加了缺陷和隱患。

在模型驗(yàn)證和時(shí)間驗(yàn)證領(lǐng)域，UPPAAL為目前較為成熟的驗(yàn)證工具。UPPAAL是瑞典Uppsala大學(xué)和丹麥Aalborg大學(xué)聯(lián)合制作的基于時(shí)間自動(dòng)機(jī)（Timed?Automata）的實(shí)時(shí)系統(tǒng)驗(yàn)證模擬工具。在UPPAAL中，過程被描述為由有限控制結(jié)構(gòu)、實(shí)數(shù)值時(shí)鐘和變量組成的時(shí)間自動(dòng)機(jī)，過程之間通過管道channel、共享變量通信、管道用于保證不同自動(dòng)機(jī)的兩個(gè)轉(zhuǎn)換同時(shí)進(jìn)行。UPPAAL自1995年提出以來(lái)，以其強(qiáng)大高效的模擬驗(yàn)證能力，在工業(yè)界和研究界被廣泛認(rèn)可和接受。

同時(shí)，為了為建模人員提供更廣泛的建模技術(shù)支持，OMG組織推出了最新的實(shí)時(shí)嵌入式系統(tǒng)建模標(biāo)準(zhǔn)，MARTE。特別是在實(shí)時(shí)建模領(lǐng)域，MARTE為系統(tǒng)設(shè)計(jì)師提供了豐富的時(shí)間建模和解決方案。MARTE時(shí)間模型結(jié)構(gòu)的包圖如圖1所示。MARTE支持多時(shí)鐘（multi?time），多種類時(shí)鐘以及多形態(tài)時(shí)鐘(multiform?time)，并且結(jié)合了VSL（value?specification?language）語(yǔ)言和CCSL，將系統(tǒng)約束以更清晰的語(yǔ)義、更標(biāo)準(zhǔn)的語(yǔ)法形式表達(dá)。

然而，對(duì)于采用MARTE建模的實(shí)時(shí)系統(tǒng)模型，目前缺乏全面完善的模型驗(yàn)證理論和實(shí)踐方法。而構(gòu)件間交互的一致性以及時(shí)間正確性等因素又是對(duì)系統(tǒng)安全的重要考量因素。?

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

本發(fā)明的目的是針對(duì)現(xiàn)有技術(shù)的不足而提供的一種以驗(yàn)證工具UPPAAL為基礎(chǔ)的模型驗(yàn)證方法，該方法能夠?qū)?shí)時(shí)嵌入式系統(tǒng)交互的一致性和時(shí)間的正確性進(jìn)行驗(yàn)證，從而減少了以模型為基礎(chǔ)的構(gòu)件在實(shí)際操作中產(chǎn)生錯(cuò)誤的概率；本發(fā)明將常用的實(shí)時(shí)嵌入式系統(tǒng)的模型轉(zhuǎn)化為工具UPPAAL能夠驗(yàn)證的時(shí)間自動(dòng)機(jī)模型，通過UPPAAL的驗(yàn)證結(jié)果，對(duì)模型采取改進(jìn)措施。

本發(fā)明的目的是這樣實(shí)現(xiàn)的：

一種基于UPPAAL的實(shí)時(shí)嵌入式系統(tǒng)構(gòu)件間協(xié)同行為的驗(yàn)證方法，該方法是:將對(duì)實(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ī)；具體包括：

將構(gòu)件的每一個(gè)端口建模成一個(gè)時(shí)間自動(dòng)機(jī)；然后，根據(jù)CCSL語(yǔ)義對(duì)端口之間交互的約束，對(duì)端口之間的交互行為信息進(jìn)行提取，并將這些行為信息建模成為模型中的主時(shí)間自動(dòng)機(jī)，用于系統(tǒng)構(gòu)件的模擬和驗(yàn)證；

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

將模型中的MARTE順序圖轉(zhuǎn)化為監(jiān)控自動(dòng)機(jī)的過程是：模型驗(yàn)證是通過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)控；

將模型中的MARTE狀態(tài)圖轉(zhuǎn)化為時(shí)間自動(dòng)機(jī)的過程是：?MARTE狀態(tài)圖對(duì)應(yīng)地為一個(gè)系統(tǒng)構(gòu)件建模；構(gòu)件內(nèi)部的事件信息通過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)；

b、使用工具UPPAAL對(duì)轉(zhuǎn)化好的時(shí)間自動(dòng)機(jī)模型進(jìn)行驗(yàn)證（如死鎖驗(yàn)證、安全攸關(guān)變量的驗(yàn)證等），并輸出驗(yàn)證結(jié)果。