擴展cCSP的操作語義及驗證技術研究.pdf

1、面向服務的計算（SOC）為分布式計算提供了一種新的方式，在SOC模式下，一個任務通常需要不同服務的協(xié)作來完成，并且這樣的協(xié)作經常需要第三方來實施。由于第三方不能夠有效隔離服務的提供方，使得傳統(tǒng)的ACID事務模型和兩段協(xié)議并不適用于SOC中服務協(xié)作的場景。在此背景下，長事務中的一致性保證機制已經成為分布式環(huán)境下服務一致性保證的重要方法。為了確保長事務的正確性，現(xiàn)階段提出了多種形式化語言來對長事務進行規(guī)約和驗證，cCSP是CSP語言面向長事

2、務的擴展，而擴展cCSP在cCSP的基礎上添加了進程并發(fā)、非確定性選擇、遞歸、重命名、隱藏等建模功能，能夠對分布式系統(tǒng)下的長事務進行有效建模。但是，當前擴展 cCSP僅有指稱語義，沒有完整的操作語義。此外，到目前為止，擴展cCSP并沒有相應的建模和驗證工具支持。為此，本文研究了擴展cCSP的操作語義，以及擴展cCSP的模型檢驗問題，并基于操作語義實現(xiàn)了擴展cCSP的模型檢驗工具。本文的主要工作如下。
　　本文基于已有的cCSP操作

3、語義，提出了擴展cCSP的操作語義，解決了已有cCSP的語義規(guī)則不完備的問題，為每個擴展cCSP中的操作給出了語義規(guī)則。在此基礎上，研究了失敗發(fā)散語義與操作語義的關聯(lián)關系，證明了兩種語義模型的一致性。研究了擴展cCSP的正規(guī)性質驗證問題的復雜性，通過將擴展cCSP正規(guī)性質驗證問題歸結到已知不可判定的Minsky2-計數(shù)器停機問題，證明了問題的不可判定性。在操作語義的基礎上，基于模型檢驗工具平臺PAT（Process Analysis T