基于自動機理論的UML模型一致性研究.pdf

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

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