支持模型驅(qū)動開發(fā)的體系結(jié)構(gòu)形式化語義與轉(zhuǎn)換一致性研究.pdf

1、模型驅(qū)動開發(fā)(Model-DrivenDevelopment，MDD)已成為軟件工程技術(shù)的研究熱點和發(fā)展趨勢，它通過提升抽象層次來應(yīng)對軟件開發(fā)的復雜性。模型轉(zhuǎn)換是MDD方法中的一項關(guān)鍵技術(shù)，模型間的映射關(guān)系是模型轉(zhuǎn)換的基礎(chǔ)和依據(jù)。但目前關(guān)于模型轉(zhuǎn)換的研究成果大都集中在模型操作的描述方面，其目的是實現(xiàn)轉(zhuǎn)換過程的自動執(zhí)行，而在映射關(guān)系的定義原則，以及轉(zhuǎn)換規(guī)則的可行性和正確性驗證等方面，還缺乏堅實的理論基礎(chǔ)，從而導致了MDD研究的理論和實現(xiàn)不

2、完善，模型轉(zhuǎn)換難以滿足實際需要的現(xiàn)狀。 模型轉(zhuǎn)換的正確性問題是所有基于模型驅(qū)動的軟件工程實施的基礎(chǔ)問題，也是模型驅(qū)動開發(fā)研究的核心問題。模型轉(zhuǎn)換正確性的一般標準包括語法正確性、語法完備性、可終止性、合流性和語義一致性。在這幾個轉(zhuǎn)換標準的判定上，除語義一致性外，其它幾個語法層次上的正確性問題都已有相對成熟的解決方案。而在模型轉(zhuǎn)換的語義一致性驗證和分析方面，目前還沒有成熟的理論基礎(chǔ)和驗證工具，模型轉(zhuǎn)換中語義特性保持的定義、描述和驗證

3、仍是一個尚未解決的難題。如何保證模型轉(zhuǎn)換前后的語義一致性，是模型驅(qū)動方法走向?qū)崿F(xiàn)的關(guān)鍵。但在目前的MDD實現(xiàn)方法中，形式化語義的缺乏使得高層模型的描述還不夠完備、精確，難以有效的支持模型轉(zhuǎn)換和代碼生成，也不能建立有效的評價和驗證機制。缺乏模型轉(zhuǎn)換相關(guān)的語義特性描述和計算，是當前基于MDD的軟件開發(fā)研究中所缺乏的主要理論。建立模型轉(zhuǎn)換相關(guān)的語義描述和計算理論是促進MDD方法健康快速發(fā)展的基礎(chǔ)和當務(wù)之急。 國內(nèi)外多年的實踐和市場的驗

4、證表明，軟件體系結(jié)構(gòu)和MDD的結(jié)合在軟件的快速開發(fā)、隨需應(yīng)變、質(zhì)量保證以及成本控制等方面是成功的，有很好的發(fā)展前景。基于以上的應(yīng)用背景和需求，本文立足于解決模型轉(zhuǎn)換的基礎(chǔ)理論和技術(shù)問題，吸收軟件體系結(jié)構(gòu)和軟件形式化等方面的研究成果，在對模型轉(zhuǎn)換過程和方法進行深入研究的基礎(chǔ)上，重點研究了軟件體系結(jié)構(gòu)模型及其間映射關(guān)系的形式化語義描述，以此為基礎(chǔ)，對模型轉(zhuǎn)換應(yīng)保持的語義特性進行了分析和探討，并開發(fā)了原型系統(tǒng)對研究成果進行了應(yīng)用和驗證。本文主

5、要的研究內(nèi)容和創(chuàng)新工作包括： (1)對模型轉(zhuǎn)換過程和方法的研究。從模型描述語言的分析入手，討論了模型轉(zhuǎn)換和模型映射的一致性需求，并對模型轉(zhuǎn)換的過程和已提出的模型轉(zhuǎn)換方法進行了綜述和歸結(jié)。借助于形式語言的擴展機制，提出了基于概念集重構(gòu)的模型映射定義方法，討論了模型描述語言之間映射關(guān)系的建立過程以及所應(yīng)遵循的基本原則，并重點分析了不同抽象層次結(jié)構(gòu)模型之間的映射關(guān)系定義和轉(zhuǎn)換的構(gòu)造過程。依據(jù)體系結(jié)構(gòu)模型的抽象定義，提出了基于體系結(jié)構(gòu)映

6、射的模型轉(zhuǎn)換理論架構(gòu)，從而為基于軟件體系結(jié)構(gòu)的模型轉(zhuǎn)換一致性研究奠定了理論基礎(chǔ)。 (2)建立了體系結(jié)構(gòu)模型及其映射關(guān)系的形式化語義描述方法。在對陸汝鈐院士提出的類型范疇理論進行擴展的基礎(chǔ)上，將其與代數(shù)規(guī)范和進程代數(shù)相結(jié)合，為軟件體系結(jié)構(gòu)模型以及模型間的映射關(guān)系提供了一種統(tǒng)一的語義描述框架。模型的結(jié)構(gòu)語義由類型范疇圖表來指代，行為語義則由范疇附帶的進程行為跡來表示，模型間的映射關(guān)系用范疇理論中的態(tài)射和函子來形式化描述。該描述機制通

7、用性強，通過將一系列小的局部映射的結(jié)果組合在一起形成大的復合結(jié)構(gòu)，以一種漸增的方式來描述抽象模型到具體實現(xiàn)的轉(zhuǎn)換關(guān)系，從而為局部映射的組合提供了一種可行的思路和方法。使用范疇理論作為數(shù)學框架，使得所討論的問題可以用與特定應(yīng)用領(lǐng)域無關(guān)的術(shù)語來形式化描述。范疇理論支持圖形化建模，可以使模型中的構(gòu)件關(guān)系以及結(jié)構(gòu)特征可視化，有利于對模型轉(zhuǎn)換的理解和追蹤。應(yīng)用研究表明，該描述框架很好地把握了模型驅(qū)動開發(fā)的實質(zhì)、過程和要求，為模型轉(zhuǎn)換和模型驅(qū)動的軟

8、件開發(fā)提供了新的認知、設(shè)計和語義計算的指導架構(gòu)。本文是首次將類型范疇理論用于研究模型的組織結(jié)構(gòu)和模型間的轉(zhuǎn)換關(guān)系，將為其他學者研究軟件模型的轉(zhuǎn)換問題提供一種新的思路。 (3)對體系結(jié)構(gòu)模型轉(zhuǎn)換所應(yīng)保持的語義特性進行了研究。分析了模型轉(zhuǎn)換過程中的語義遷移。基于軟件體系結(jié)構(gòu)模型的形式化描述，從結(jié)構(gòu)語義、公理語義、端口語義和行為語義等幾個方面分析了模型轉(zhuǎn)換中特性保持問題的描述，并建立了相應(yīng)的判定標準，同時探討了證明一個轉(zhuǎn)換是否滿足某些

9、特性保持約束的方法。這些方法支持以定理證明的方式，對模型轉(zhuǎn)換的語義特性保持進行驗證，克服了模型檢測的不足。該研究可用于指導模型轉(zhuǎn)換規(guī)則的定義，為模型映射關(guān)系的正確性驗證提供依據(jù)，從而為進一步全面研究模型轉(zhuǎn)換所應(yīng)遵循的法則和特性奠定基礎(chǔ)。本文是首次提出從體系結(jié)構(gòu)模型之間的映射關(guān)系所表達的模型復合的語義的一致性來考察模型轉(zhuǎn)換的正確性，在模型驅(qū)動開發(fā)研究領(lǐng)域是一次新的嘗試。 (4)在開發(fā)和應(yīng)用方面，開發(fā)了模型驅(qū)動方法的原型工具，并完成

10、了一系列的工程應(yīng)用。從軟件體系結(jié)構(gòu)建模出發(fā)，通過對UML進行擴展，提出了一種包括體系結(jié)構(gòu)模型、靜態(tài)視圖、邏輯視圖和界面展示視圖四部分的WEB應(yīng)用模型描述方法。然后依據(jù)體系結(jié)構(gòu)模型轉(zhuǎn)換一致性研究的理論和方法定義模型轉(zhuǎn)換規(guī)則，實現(xiàn)了向J2EE平臺和ASP.NET平臺的模型轉(zhuǎn)換和代碼生成，從而驗證了本文所提理論和方法的合理性和實用性。 本文的研究成果豐富和完善了MDD方法的理論架構(gòu)，為模型驅(qū)動的軟件開發(fā)研究提供了一種新的思路，對于促進