基于動態(tài)邏輯的UML模型一致性檢驗.pdf

1、在基于UML的軟件開發(fā)過程中，各種UML圖形從不同側(cè)面描繪著所開發(fā)的軟件系統(tǒng)，這些圖形之間存在著信息的重疊，從而導致UML模型的一致性問題。UML模型的一致性問題也是建模過程中一個重要并且需要解決的問題。 KeY Tool是一個支持形式化規(guī)范和代碼驗證的工具，該工具基于動態(tài)邏輯對程序和形式化規(guī)范進行分析和驗證，然而該工具并不支持在設計階段對UML模型進行一致性檢驗。作為KeY Fool的基礎，動態(tài)邏輯不僅具備描述程序設計語言的能

2、力，而且能夠描述UML/OCL中的動態(tài)概念。因此，研究利用動態(tài)邏輯來解決UML 模型的一致性問題具有理論意義和應用價值。 本論文首先對UML模型存在的一致性問題進行綜述，在此基礎上深入分析已有的方法，即Greg提出的利用動態(tài)邏輯來檢驗UML模型一致性的方法中存在的問題。Greg的方法只針對某一特定簡單的UML模型進行設計，而本論文從一般UML模型的基本要素出發(fā)來分析模型轉(zhuǎn)換的方法，解決了原有方法中存在的一些問題。并且，原有方法只