基于UPPAAL和UML的實(shí)時(shí)系統(tǒng)形式化分析與應(yīng)用.pdf

1、計(jì)算機(jī)的應(yīng)用模式在經(jīng)歷了主機(jī)模式和個(gè)人機(jī)模式后，目前正向最適合人類使用的普適計(jì)算模式發(fā)展。在普適計(jì)算模式下，實(shí)時(shí)系統(tǒng)將會(huì)滲透到人們生活的方方面面，為提高人們的生活質(zhì)量發(fā)揮重要的作用。在這種情況下，實(shí)時(shí)系統(tǒng)的質(zhì)量和開(kāi)發(fā)效率往往會(huì)對(duì)一個(gè)產(chǎn)品的成功起著決定性的影響。為了保障實(shí)時(shí)系統(tǒng)的實(shí)時(shí)性、安全性和可靠性等，本文在深入研究了時(shí)間自動(dòng)機(jī)、UPPAAL、UML的理論基礎(chǔ)上，采用時(shí)間自動(dòng)機(jī)與UML相結(jié)合的建模方法，使用UPPAAL，對(duì)所建模型進(jìn)行分

2、析與驗(yàn)證，并結(jié)合兩個(gè)實(shí)例說(shuō)明了本方法。 采用形式化方法對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行分析和驗(yàn)證是提高其安全性、可靠性的一條重要途徑。目前時(shí)間自動(dòng)機(jī)是用于實(shí)時(shí)系統(tǒng)建模的重要形式化工具，它刻畫(huà)了實(shí)時(shí)系統(tǒng)與時(shí)間有關(guān)的行為特征，反映了實(shí)時(shí)系統(tǒng)控制行為的可視轉(zhuǎn)向。UML順序圖著重體現(xiàn)對(duì)象間動(dòng)態(tài)的交互關(guān)系，而且具有良好的易理解性。但是UML順序圖用來(lái)對(duì)實(shí)時(shí)系統(tǒng)建模和驗(yàn)證還存在時(shí)間描述方面的不足，因此本文研究了利用UMI，的擴(kuò)展機(jī)制對(duì)UML順序圖進(jìn)行擴(kuò)展的方