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

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

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

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

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

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

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

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

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

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

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