基于進程代數(shù)和模型檢驗的系統(tǒng)建模與評價

1、東南大學(xué)博士學(xué)位論文基于進程代數(shù)和模型檢驗的系統(tǒng)建模與評價姓名：劉園申請學(xué)位級別：博士專業(yè)：計算機應(yīng)用技術(shù)指導(dǎo)教師：徐寶文20080120提出了一種基于跡的連續(xù)隨機時序邏輯tCSL(TracebasedContinousStochasticLo西c)，并給出了ALSTS’系統(tǒng)從隨機進程代數(shù)建模到tCSL模型檢驗的性能評價方法CSL(ContinuousStochasticLogic)時序邏輯不含動作的概念，因此無法針對變遷動作進行分析。

2、aCSL(actionlabeledContinuousStochasticLogic)雖然可以分析變遷過程中的動作，但不能分析動作的執(zhí)行順序，本文在CSL和aCSL的基礎(chǔ)上增加了動作的概念、關(guān)鍵路徑的概念及跡關(guān)鍵動作的概念，描述了tCSL的詞法和語義。對不限時與限時的。Next”和“Until”時序操作給出了基于關(guān)鍵路徑和關(guān)鍵動作的穩(wěn)態(tài)概率分析，重點闡述了針對路徑的tcsL模型檢驗的方法，并通過實例分析，結(jié)合ALSTS’系統(tǒng)的隨機進程

3、代數(shù)建模，實現(xiàn)了對關(guān)鍵動作序列有要求的路徑相關(guān)的系統(tǒng)性能評價。并給出了tCSL模型檢驗平臺支撐工具原型。借助跡關(guān)鍵動作和瞬時內(nèi)部動作，給出了～種非確定性隨機系統(tǒng)向ALSTS’系統(tǒng)轉(zhuǎn)換的方法，從而可使用tcsL模型檢驗方法對重構(gòu)后的非確定性系統(tǒng)進行路徑相關(guān)的系統(tǒng)性能評價。本文還提出了跡互模擬等價的概念，給出了跡瓦模擬等價性定理。利用跡互模擬等價性，可對系統(tǒng)的狀態(tài)窄問進行壓縮，并能保留關(guān)鍵路徑和關(guān)鍵動作的信息。關(guān)鍵詞進程代數(shù)、模型檢驗，并發(fā)