基于Petri網(wǎng)的嵌入式系統(tǒng)建模與驗(yàn)證研究.pdf

1、隨著嵌入式系統(tǒng)在各個(gè)領(lǐng)域的廣泛應(yīng)用，嵌入式系統(tǒng)變得越來(lái)越復(fù)雜。在嵌入式系統(tǒng)設(shè)計(jì)中采用模型的方法，有利于確保系統(tǒng)的正確性，縮短開(kāi)發(fā)周期，降低開(kāi)發(fā)費(fèi)用。本文以Perti網(wǎng)為建模工具，對(duì)嵌入式系統(tǒng)的建模和分析驗(yàn)證進(jìn)行了一些研究。
　　 嵌入式系統(tǒng)具有實(shí)時(shí)性、并發(fā)性等特點(diǎn)，并要求高可靠性和正確性。為了設(shè)計(jì)具有這樣特點(diǎn)的系統(tǒng)，設(shè)計(jì)過(guò)程必須基于一個(gè)形式化描述，以捕獲嵌入式系統(tǒng)的這些特點(diǎn)。Petri網(wǎng)對(duì)這類(lèi)系統(tǒng)是一個(gè)很好的描述方法：可以表示并

2、行和連續(xù)活動(dòng)，并且很容易捕捉不確定性行為。但傳統(tǒng)的Petri網(wǎng)缺乏時(shí)間概念和數(shù)據(jù)表達(dá)力，不能很好的描述嵌入式系統(tǒng)的實(shí)時(shí)性要求和數(shù)據(jù)流。針對(duì)傳統(tǒng)Petri網(wǎng)的這些缺點(diǎn)，本文提出基于PRES+的嵌入式系統(tǒng)的建模與分析驗(yàn)證研究。
　　 首先，介紹嵌入式系統(tǒng)的一個(gè)形式化計(jì)算模型PRES+，可以描述嵌入式系統(tǒng)的一些重要特征，其中，托肯攜帶數(shù)據(jù)信息，變遷執(zhí)行數(shù)據(jù)的轉(zhuǎn)換，時(shí)間通過(guò)與變遷相連的活動(dòng)期限來(lái)捕獲。同時(shí)，引入PRES+模型的分層機(jī)制和

3、組合修改操作。分層機(jī)制使模型能夠有條理的構(gòu)建，由簡(jiǎn)單的單元組件構(gòu)成，使得設(shè)計(jì)師在每個(gè)描述級(jí)上都可以很容易理解；組合修改操作，通過(guò)增加或減少模塊來(lái)改變其功能或狀態(tài)，從而以最小的影響，實(shí)現(xiàn)了網(wǎng)模型的修改，并有效保存了系統(tǒng)的性質(zhì)，使系統(tǒng)在修改后不需要再重新驗(yàn)證其性質(zhì)。
　　 其次，介紹了系統(tǒng)模型的分析與驗(yàn)證，對(duì)基于PRES+建模的嵌入式系統(tǒng)，分別提出兩種方法，對(duì)它進(jìn)行分析驗(yàn)證。第一種為形式化驗(yàn)證方法，利用模型檢測(cè)來(lái)驗(yàn)證系統(tǒng)的一些性質(zhì)，