發(fā)布時間：2017-07-19 12:00

  本文關(guān)鍵詞：電子商務(wù)環(huán)境中業(yè)務(wù)流程的形式化分析與驗證

  更多相關(guān)文章： 電子商務(wù) 業(yè)務(wù)流程 行為時序邏輯 形式化分析與驗證 Petri網(wǎng) 業(yè)務(wù)流程執(zhí)行語言

【摘要】：飛速發(fā)展的計算機(jī)網(wǎng)絡(luò)被廣泛應(yīng)用于各領(lǐng)域，正在引領(lǐng)社會和經(jīng)濟(jì)的深刻變革。計算機(jī)網(wǎng)絡(luò)已經(jīng)成為人們生活和工作中的一個不可或缺的組成部分，基于計算機(jī)網(wǎng)絡(luò)的“電子商務(wù)”正在迅猛發(fā)展。隨著信息技術(shù)的快速發(fā)展和電子商務(wù)的廣泛應(yīng)用，傳統(tǒng)業(yè)務(wù)流程已不能適應(yīng)企業(yè)新的發(fā)展需要。業(yè)務(wù)流程的設(shè)計、建模、優(yōu)化、重組及耦合等逐漸成為研究熱點，為保證業(yè)務(wù)流程安全可靠和高效，必須借助形式化方法嚴(yán)格描述和驗證業(yè)務(wù)流程。當(dāng)代的企業(yè)要適應(yīng)電子商務(wù)環(huán)境，必須使其業(yè)務(wù)流程符合電子商務(wù)環(huán)境中業(yè)務(wù)流程的特征，電子商務(wù)環(huán)境下的業(yè)務(wù)流程形式化分析是非常必要的。 目前國內(nèi)外還缺乏針對電子商務(wù)環(huán)境下的業(yè)務(wù)流程進(jìn)行準(zhǔn)確形式化分析方法體系和自動驗證，選題比較系統(tǒng)地研究分析電子商務(wù)環(huán)境下企業(yè)業(yè)務(wù)流程日益動態(tài)化、并發(fā)、柔性和跨組織等特性，研究如何把這些新特性引入行為時序邏輯，對TLA進(jìn)行擴(kuò)展，可以豐富業(yè)務(wù)流程形式化方法理論體系。對Petri網(wǎng)進(jìn)行概述，分析Petri網(wǎng)如何轉(zhuǎn)換到TLA，并提出進(jìn)一步擴(kuò)展的方法。介紹了業(yè)務(wù)流程執(zhí)行語言BPEL，分析BPEL如何擴(kuò)展到TLA，分析進(jìn)一步擴(kuò)展的可行性。本文使用行為時序邏輯TLA建模與仿真方法及其自動模型檢測工具，對電子商務(wù)環(huán)境下的業(yè)務(wù)流程進(jìn)行形式化分析與驗證，可為企業(yè)實施業(yè)務(wù)流程再造提供理論基礎(chǔ)和技術(shù)保障，豐富和發(fā)展業(yè)務(wù)流程形式化分析及自動驗證方法理論體系，為日益復(fù)雜與動態(tài)化的業(yè)務(wù)流程分析驗證提供新思路和新方法，，可以輔助企業(yè)研究設(shè)計高效可靠的業(yè)務(wù)流程，為企業(yè)創(chuàng)造更大的經(jīng)濟(jì)效益。
【關(guān)鍵詞】：電子商務(wù) 業(yè)務(wù)流程 行為時序邏輯 形式化分析與驗證 Petri網(wǎng) 業(yè)務(wù)流程執(zhí)行語言
【學(xué)位授予單位】：貴州財經(jīng)大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2014
【分類號】：TP393.09;TP301.1
【目錄】：

• 摘要4-5
• Abstract5-8
• 1 緒論8-15
• 1.1 業(yè)務(wù)流程形式化研究8-11
• 1.1.1 業(yè)務(wù)流程研究的發(fā)展8
• 1.1.2 業(yè)務(wù)流程形式化分析的方法和國內(nèi)外研究現(xiàn)狀8-10
• 1.1.3 業(yè)務(wù)流程形式化分析和驗證的國內(nèi)外研究現(xiàn)狀10-11
• 1.2 選題的背景及意義11-13
• 1.3 本文的主要研究工作13
• 1.4 論文內(nèi)容的結(jié)構(gòu)安排13-15
• 2 行為時序邏輯 TLA15-23
• 2.1 形式化方法15-17
• 2.2 TLA 概述17-18
• 2.3 TLA 的語法與語義18-19
• 2.3.1 符號與語法18-19
• 2.3.2 基本定義與語義19
• 2.4 TLA 的應(yīng)用19-21
• 2.5 TLA~+與 TLC21-22
• 2.6 本章小結(jié)22-23
• 3 Petri 網(wǎng)及其擴(kuò)展23-35
• 3.1 Petri 網(wǎng)的定義24-25
• 3.2 Petri 網(wǎng)特性25-27
• 3.3 Petri 網(wǎng)的類型27-28
• 3.4 Petri 網(wǎng)的應(yīng)用28-31
• 3.5 Petri 網(wǎng)的擴(kuò)展31-32
• 3.6 Petri 網(wǎng)到 TLA 的轉(zhuǎn)化32-34
• 3.7 本章小結(jié)34-35
• 4 BPEL 業(yè)務(wù)流程執(zhí)行語言及其轉(zhuǎn)化35-46
• 4.1 BPEL 業(yè)務(wù)流程執(zhí)行語言35-39
• 4.1.1 BPEL 的發(fā)展過程35-36
• 4.1.2 BPEL 的結(jié)構(gòu)36-39
• 4.1.3 BPEL 的語法39
• 4.2 BPEL 的應(yīng)用39-40
• 4.3 BPEL 到 TLA 的轉(zhuǎn)化40-45
• 4.4 本章小結(jié)45-46
• 5 行為時序邏輯 TLA 的擴(kuò)展46-59
• 5.1 電子商務(wù)環(huán)境中業(yè)務(wù)流程的新特性46-48
• 5.1.1 柔性47
• 5.1.2 成本最小化47
• 5.1.3 時效性47-48
• 5.1.4 跨組織性48
• 5.2 對行為時序邏輯 TLA 進(jìn)行理論擴(kuò)充與改進(jìn)48-49
• 5.2.1 增加新的謂詞48
• 5.2.2 增加新的推演規(guī)則48-49
• 5.3 網(wǎng)上訂票業(yè)務(wù)流程描述49-57
• 5.4 本章小結(jié)57-59
• 6 總結(jié)與展望59-61
• 6.1 總結(jié)59
• 6.2 展望59-61
• 參考文獻(xiàn)61-64
• 附錄A64-65
• 致謝65

【參考文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前1條

1 劉晴晴;文靜華;;基于TLA的業(yè)務(wù)流程形式化分析[J];計算機(jī)光盤軟件與應(yīng)用;2013年07期

本文編號：562728