基于時(shí)態(tài)邏輯的UML交互模型檢測研究.pdf

1、統(tǒng)一建模語言(Unified Modeling Language，UML)是一種易理解、易描述、直觀的可視化建模語言，它提供多種模型元素從系統(tǒng)的各個(gè)角度描述系統(tǒng)性質(zhì)、功能及運(yùn)行環(huán)境，基于UML的計(jì)算機(jī)軟系統(tǒng)的分析和設(shè)計(jì)已經(jīng)廣泛地應(yīng)用于各個(gè)領(lǐng)域。UML交互模型從系統(tǒng)行為的角度細(xì)致、準(zhǔn)確地刻畫了計(jì)算機(jī)軟件系統(tǒng)的交互行為.為程序開發(fā)人員及最終用戶正確理解系統(tǒng)的交互行為提供了便捷、高效的可視化模型。對UML交互模型進(jìn)行驗(yàn)證判斷軟件系統(tǒng)模型是否滿

2、足交互的性質(zhì)成為一個(gè)重要的研究問題。 模型檢測(Model checking)是一種應(yīng)用廣泛的形式化自動(dòng)驗(yàn)證正技術(shù)，主要通過顯式狀態(tài)搜索或隱式小動(dòng)點(diǎn)汁算來驗(yàn)證系統(tǒng)的模態(tài)/命題性質(zhì)。本文采用基于自動(dòng)機(jī)理論框架下的時(shí)態(tài)邏輯模型驗(yàn)證檢測技術(shù)，對UML2.0交互模型的模型檢測進(jìn)行了研究. 為了對UML2.0交互模型進(jìn)行有關(guān)性質(zhì)的檢測，首先應(yīng)將UML2.0交互模型進(jìn)行形式化的描述，使其轉(zhuǎn)化為一種可以接受消息交換或系統(tǒng)狀態(tài)變化的自動(dòng)

3、機(jī)。在OMG發(fā)布的UML2.0交互模型可視化浯法的基礎(chǔ)上，對UML2.0交互模型的語法和語義進(jìn)行了抽象，描述了交互模型的基本語法，提出了一種形式化了描述模型的Baeks自動(dòng)機(jī)-交互自動(dòng)機(jī)在此基礎(chǔ)上，本文研究了基于交互自動(dòng)機(jī)和時(shí)態(tài)邏輯的UML交互模型性質(zhì)檢測方法，提出了模型檢測所需的Marking算法。該算法通過對交互自動(dòng)機(jī)全部狀態(tài)的遍歷，檢測各狀態(tài)的時(shí)態(tài)邏輯公式(CTL公式)的真值，以判斷用戶沒汁的UML交互摸型是符合計(jì)算機(jī)軟件系統(tǒng)應(yīng)滿