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

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

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