基于模型的實(shí)時(shí)系統(tǒng)形式化驗(yàn)證方法研究與實(shí)現(xiàn).pdf

1、隨著計(jì)算機(jī)技術(shù)的發(fā)展，尤其是實(shí)時(shí)系統(tǒng)在各個(gè)領(lǐng)域的滲透，軟件工程領(lǐng)域中對實(shí)時(shí)系統(tǒng)的功能行為、資源利用狀況、能量消耗等特性的認(rèn)識(shí)越來越深入，如何才能夠在系統(tǒng)模型設(shè)計(jì)階段保證其可靠性已經(jīng)成為領(lǐng)域內(nèi)關(guān)注的熱點(diǎn)。在系統(tǒng)開發(fā)的過程中，UML已經(jīng)成為設(shè)計(jì)人員廣泛使用的建模語言，尤其是計(jì)時(shí)圖擁有出色的時(shí)間因素表現(xiàn)能力是實(shí)時(shí)系統(tǒng)建模的不二選擇。由于UML是一種半形式化的建模語言，不能直接在其基礎(chǔ)上進(jìn)行模型驗(yàn)證，而時(shí)間自動(dòng)機(jī)模型是一種完全形式化的語言，UP

2、PAAL是基于時(shí)間自動(dòng)機(jī)的驗(yàn)證工具，可以對實(shí)時(shí)系統(tǒng)進(jìn)行實(shí)時(shí)功能驗(yàn)證。因此本文以計(jì)時(shí)圖模型作為實(shí)時(shí)系統(tǒng)的建模模型，通過模型轉(zhuǎn)換算法將其轉(zhuǎn)換為UPPAAL中的時(shí)間自動(dòng)機(jī)驗(yàn)證模型。
　　本文首先介紹了實(shí)時(shí)系統(tǒng)形式化驗(yàn)證的相關(guān)理論與技術(shù)，給出了UML計(jì)時(shí)圖和時(shí)間自動(dòng)機(jī)的形式化描述，改進(jìn)現(xiàn)有的模型轉(zhuǎn)換方法，將計(jì)時(shí)圖模型轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)。然后利用轉(zhuǎn)換后的時(shí)間自動(dòng)機(jī)進(jìn)行功能驗(yàn)證，并對時(shí)間自動(dòng)機(jī)做了進(jìn)一步的擴(kuò)展，給出了資源時(shí)間自動(dòng)機(jī)、能耗時(shí)間自動(dòng)