基于自動(dòng)機(jī)理論的UML模型一致性研究.pdf

1、隨著計(jì)算機(jī)技術(shù)的發(fā)展，軟件系統(tǒng)的復(fù)雜度也越來越高。建模是對(duì)系統(tǒng)進(jìn)行抽象的最好的辦法，模型就是對(duì)復(fù)雜問題進(jìn)行分層，從而更好地解決問題。UML自上世紀(jì)90年代產(chǎn)生至今，作為基于面向?qū)ο蠹夹g(shù)的標(biāo)準(zhǔn)建模語言，已經(jīng)被廣泛使用。UML的優(yōu)勢主要體現(xiàn)在可以使用單一的集成表示法來對(duì)系統(tǒng)的多個(gè)方面進(jìn)行建模，可以用于描述一個(gè)系統(tǒng)的靜態(tài)結(jié)構(gòu)和動(dòng)態(tài)行為。然而由UML得到的表示系統(tǒng)多個(gè)方面的模型之間存在著一定的信息冗余和相互交織，從而產(chǎn)生了一致性問題。

2、模型檢測是一種產(chǎn)生于上世紀(jì)80年代的形式化驗(yàn)證技術(shù)，目前該技術(shù)已經(jīng)相當(dāng)成熟。模型檢測技術(shù)能夠?qū)⑾到y(tǒng)的驗(yàn)證問題轉(zhuǎn)化為數(shù)學(xué)問題來解決。這種用嚴(yán)格的數(shù)學(xué)方法來推理驗(yàn)證某一產(chǎn)品或設(shè)計(jì)是否符合其全部或部分規(guī)范的技術(shù)，可以很好的應(yīng)用于高可信軟件和系統(tǒng)的實(shí)現(xiàn)過程中。 本文研究了如何使用基于自動(dòng)機(jī)理論的模型檢測技術(shù)對(duì)UML狀態(tài)圖和順序圖的一致性進(jìn)行驗(yàn)證，提出了基于Büchi自動(dòng)機(jī)理論對(duì)UML的狀態(tài)圖和順序圖進(jìn)行一致性驗(yàn)證的方法。文章對(duì)UML模型