在統(tǒng)一建模語(yǔ)言(Unified Modeling Language)UML2.0規(guī)范中，模型的語(yǔ)法是通過(guò)元模型以類圖形式定義的，靜態(tài)語(yǔ)義用對(duì)象約束語(yǔ)言(Object Constraint Language)OCL描述，動(dòng)態(tài)語(yǔ)義直接用英文的自然語(yǔ)言表達(dá)。采用這種方法描述的動(dòng)態(tài)語(yǔ)義，存在著不完全、不一致、模糊性等缺陷，為軟件開(kāi)發(fā)的后續(xù)工作帶來(lái)了不利影響：不利于對(duì)復(fù)雜系統(tǒng)的模型進(jìn)行嚴(yán)格的語(yǔ)義分析和正確性驗(yàn)證。順序圖是統(tǒng)一建模語(yǔ)言UML定義的動(dòng)態(tài)圖中最重要的圖形之一，給出其準(zhǔn)確、完整、一致的語(yǔ)義將有利于對(duì)復(fù)雜系統(tǒng)的模型進(jìn)行嚴(yán)格的語(yǔ)義分析和正確性驗(yàn)證，從而給軟件的后續(xù)開(kāi)發(fā)提供幫助。 UML 2.0版本定義的順序圖用來(lái)描述對(duì)象之間的動(dòng)態(tài)交互關(guān)系，著重體現(xiàn)對(duì)象間消息傳遞的時(shí)間順序卻沒(méi)有嚴(yán)格的時(shí)間限制，因此用一個(gè)合適的時(shí)序邏輯描述語(yǔ)言來(lái)給出它的語(yǔ)義是可行的。XYZ／E是一個(gè)可執(zhí)行線性時(shí)序邏輯語(yǔ)言，既可描述系統(tǒng)的動(dòng)態(tài)行為又可表示程序性質(zhì)。對(duì)順序圖進(jìn)行形式化規(guī)約后，就可在統(tǒng)一的時(shí)序邏輯框架下分析順序圖的性質(zhì)。 UML2.0順序圖的組成元素用XYZ／E很難直接表示出準(zhǔn)確、完整、一致的語(yǔ)義，因此本課題的一個(gè)關(guān)...

【文章頁(yè)數(shù)】：54 頁(yè)

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
Abstract
第一章 前言
    1.1 綜述
    1.2 研究現(xiàn)狀介紹
    1.3 研究方法和目標(biāo)以及本文的組織安排
第二章 形式化方法與時(shí)序邏輯語(yǔ)言XYZ/E
    2.1 形式化方法與規(guī)范語(yǔ)言
    2.2 線性時(shí)序邏輯語(yǔ)言XYZ/E簡(jiǎn)介
    2.3 XYZ/BE的組成成分介紹
第三章 統(tǒng)一建模語(yǔ)言UML及其順序圖
    3.1 統(tǒng)一建模語(yǔ)言UML
    3.2 UML2.0順序圖介紹
    3.3 對(duì)象約束語(yǔ)言O(shè)CL(Object Constraint Language)
第四章 從順序圖到并發(fā)控制流圖的轉(zhuǎn)換
    4.1 為順圖選擇合適的控制流模型
    4.2 UML2.0活動(dòng)圖
    4.3 并發(fā)控制流圖(CCFG)
    4.4 從順序圖到并發(fā)控制流圖CCFG的轉(zhuǎn)換規(guī)則
第五章 用 XYZ/E描述基于 CCFG的UML2.0順序圖的語(yǔ)義
    5.1 CCFG的語(yǔ)法與約束
    5.2 CCFG的形式化語(yǔ)義
    5.3 案例研究:圖書管理系統(tǒng)
第六章 總結(jié)
參考文獻(xiàn)
攻讀學(xué)位期間的研究成果
致謝



本文編號(hào)：3855072