基于進(jìn)程代數(shù)和模型檢驗(yàn)的系統(tǒng)建模與評(píng)價(jià)

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

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

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