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

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