UML狀態(tài)機(jī)的形式化語義研究.pdf

1、目前,很多機(jī)構(gòu)和個(gè)人都在從事UML的形式語義研究,他們試圖通過對UML的研究來對UML的未來產(chǎn)生影響.這些機(jī)構(gòu)和個(gè)人所采用的方法主要是補(bǔ)充法和具有面向?qū)ο髷U(kuò)展的形式語言方法.這兩種方法各具有優(yōu)點(diǎn),但是也存在不足.在補(bǔ)充法中所使用的形式化語言不具有面向?qū)ο蟮奶卣?不能很好地和當(dāng)前實(shí)踐相結(jié)合,而具有面向?qū)ο髷U(kuò)展的形式語言方法又不能直接對UML模型的語義進(jìn)行形式化,影響了讀者對UML模型形式化的理解.針對以上不足,作者將上述兩種方法結(jié)合起來,

2、提出了一種新的形式化狀態(tài)機(jī)語義的方法,即首先對UML狀態(tài)機(jī)的元模型的語法結(jié)構(gòu)進(jìn)行分析,然后通過具有面向?qū)ο筇卣鞯腞AISE(Rigorous Approach to Industry SoftwareEngineering)的說明語言RSL(RAISE Specification Language)直接對UML狀態(tài)機(jī)的操作語義進(jìn)行形式化.其中在對語法結(jié)構(gòu)分析這一部分中,作者通過提出一個(gè)狀態(tài)層次結(jié)構(gòu)對UML狀態(tài)機(jī)的各種狀態(tài)及其間的相互關(guān)系

3、進(jìn)行分析,然后依次對事件、轉(zhuǎn)換的結(jié)構(gòu)進(jìn)行分析,最后對UML狀態(tài)機(jī)的語法結(jié)構(gòu)進(jìn)行了總結(jié)性形式化描述.在對UML狀態(tài)機(jī)的"運(yùn)行到完成"這一基本操作的語義進(jìn)行形i式化中,作者運(yùn)用RSL語言,依次對轉(zhuǎn)換的成立、轉(zhuǎn)換的沖突、沖突的解決、轉(zhuǎn)換的選擇的沿義進(jìn)行了形式化描述,并最終提出一個(gè)UML狀態(tài)機(jī)"運(yùn)行到完成"操作的算法.通過上述這兩部分的結(jié)合,從而提出了一個(gè)完整的UML狀態(tài)機(jī)語義形式化的新方法.最后,作者通過一個(gè)實(shí)例說明UML狀態(tài)機(jī)語義的形式化描