發(fā)布時間：2020-11-20 07:16

　　 移動分布式系統(tǒng)中的計算描述的是如何向分布在不同位置的用戶提供高質量的信息服務,目前已經被廣泛地應用于教育科研、國防軍事、交通運輸和航空航天等領域。移動計算的移動性和本身所處的環(huán)境會顯著地影響通信質量,可能會導致原本可以通信的雙方無法繼續(xù)通信。因此如何刻畫移動計算的特征和環(huán)境從而提高服務質量成為重要的研究點。本文使用形式化方法對移動分布式系統(tǒng)開展了研究,提出了移動分布式系統(tǒng)的進程演算BigrTiMo。和現(xiàn)有的演算相比,我們的演算不但捕捉了移動計算的移動性,還刻畫了移動計算的空間結構和時間特性。在形式語義學的指導下,本文研究了BigrTiMo演算的操作語義,并在Maude工具中對語義規(guī)則進行了實現(xiàn)。在圖靈獎獲得者C.A.R.Hoare教授和何積豐院士所提出的程序統(tǒng)一理論的指導下,本文研究了BigrTiMo演算的指稱語義、代數(shù)語義和語義連接理論,集中研究了從代數(shù)語義生成操作語義和指稱語義�；�于霍爾邏輯,本文研究了BigrTiMo演算的證明系統(tǒng),該證明系統(tǒng)用于驗證程序的正確性。本文的主要內容和貢獻包括如下幾點:·本文提出了移動分布式系統(tǒng)的進程演算BigrTiMo,該演算結合了rTiMo演算和圖靈獎獲得者Robin Milner教授的偶圖模型。rTiMo演算只可以建模局部通信,為了支持遠程通信的建模,我們在rTiMo演算的基礎上引入了偶圖模型,從而提出了BigrTiMo演算。我們的演算不但可以描述移動性,還可以刻畫空間結構和時間特性�！け疚难芯苛薆igrTiMo演算的語義模型,包括操作語義、指稱語義、代數(shù)語義和證明系統(tǒng)。操作語義直觀地刻畫了程序運行的過程�；�于重寫引擎Maude,我們對演算的操作語義進行了重寫并對實際生活案例進行了仿真和驗證。指稱語義基于數(shù)學理論,以更加抽象的方式刻畫了程序的行為。代數(shù)語義由一系列的代數(shù)規(guī)則組成,為了支持代數(shù)并發(fā)規(guī)則的研究,我們引入了衛(wèi)兵選擇的概念。基于指稱語義,我們證明了代數(shù)規(guī)則的正確性。證明系統(tǒng)是由一系列的證明規(guī)則組成,用于驗證程序的正確性。我們證明了證明系統(tǒng)的可靠性并通過案例展示了證明系統(tǒng)的應用。·本文研究了語義連接,主要研究了從代數(shù)語義生成操作語義和指稱語義。為了支持語義的生成,我們引入了首規(guī)范型的概念,基于首規(guī)范型,我們定義了生成策略,從而生成了變遷系統(tǒng)(操作語義)和指稱語義。我們證明了變遷系統(tǒng)和生成策略的等價性,揭示了操作語義的正確性和完備性。
【學位單位】：華東師范大學
【學位級別】：博士
【學位年份】：2019
【中圖分類】：TN929.5
【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景和動機
    1.2 研究現(xiàn)狀和相關工作
    1.3 本文的主要工作和架構
第二章 基礎理論和指導方法
    2.1 進程演算
    2.2 rTiMo演算的語法
    2.3 偶圖模型
    2.4 形式語義學
    2.5 程序統(tǒng)一理論
    2.6 Maude概述
第三章 移動分布式系統(tǒng)的進程演算BigrTiMo
    3.1 BigrTiMo演算的語法
    3.2 BigrTiMo演算的操作語義
    3.3 基于Maude的仿真與驗證
    3.4 本章小結
第四章 BigrTiMo演算的指稱語義
    4.1 語義模型與健康條件
    4.2 基本命令的指稱語義
    4.3 衛(wèi)兵選擇的指稱語義
    4.4 并發(fā)組合的指稱語義
    4.5 本章小結
第五章 BigrTiMo演算的代數(shù)語義及其語義連接
    5.1 BigrTiMo演算的代數(shù)語義
    5.2 首規(guī)范型
    5.3 代數(shù)語義和操作語義之間的連接
    5.4 代數(shù)語義和指稱語義之間的連接
    5.5 本章小結
第六章 BigrTiMo演算的證明系統(tǒng)
    6.1 描述規(guī)范
    6.2 證明規(guī)則
    6.3 證明系統(tǒng)的可靠性
    6.4 證明系統(tǒng)的應用案例
    6.5 本章小結
第七章 總結與展望
    7.1 本文工作總結
    7.2 后續(xù)工作展望
參考文獻
致謝
攻讀博士學位期間發(fā)表論文和科研情況

【相似文獻】

相關期刊論文 前10條

1 沈濤;;分布式系統(tǒng)動目標防御[J];通信對抗;2016年04期

2 黃煒耀;;分布式系統(tǒng)中的周期性事件實現(xiàn)研究[J];信息通信;2017年09期

3 ;分布式系統(tǒng)概念與設計[J];計算機教育;2013年08期

4 George Coulouri;Jean Dollimore;Tim Kindberg;Gordon Blair;;分布式系統(tǒng)概念與設計[J];計算機教育;2013年10期

5 George Coulouris;Jean Dollimore;Tim Kindberg;Gordon Blair;;分布式系統(tǒng)概念與設計[J];計算機教育;2013年12期

6 姜冬;王慧強;馮光升;呂宏武;林俊宇;;基于模糊層次化評估的分布式系統(tǒng)自毀感知方法及應用[J];小型微型計算機系統(tǒng);2012年04期

7 陳建英;楊憲澤;張楠;;面向大規(guī)模分布式系統(tǒng)的多級緩存信息結構研究[J];西南民族大學學報(自然科學版);2012年03期

8 況曉輝;趙剛;溫研;許飛;苗青;;大規(guī)模分布式系統(tǒng)脆弱性分析框架研究[J];計算機科學;2012年06期

9 趙剛;趙金晶;況曉輝;鄭緯民;;大規(guī)模分布式系統(tǒng)實體交互脆弱性分析方法[J];計算機工程與應用;2011年18期

10 杜文晟;;淺論分布式系統(tǒng)中間件的安全[J];湖北師范學院學報(自然科學版);2010年01期

相關博士學位論文 前10條

1 謝宛玲;移動分布式系統(tǒng)的進程演算BigrTiMo及其形式語義研究[D];華東師范大學;2019年

2 梅晶;并行分布式系統(tǒng)中的節(jié)能調度策略與算法研究[D];湖南大學;2015年

3 童釗;基于計算智能的并行分布式系統(tǒng)任務調度算法研究[D];湖南大學;2014年

4 李晉國;分布式系統(tǒng)中的安全協(xié)議研究[D];湖南大學;2014年

5 彭艦;基于CORBA的分布式系統(tǒng)中實時—容錯性的研究——分布式系統(tǒng)中動態(tài)調度的設計與實現(xiàn)[D];電子科技大學;2004年

6 鄧超;面向Agent的智能化分布式計算及其應用研究[D];浙江大學;2005年

7 呂毅;證明和測試分布式系統(tǒng)的功能正確性[D];中國科學院研究生院（計算技術研究所）;2004年

8 龔奕利;分布式環(huán)境中的資源發(fā)現(xiàn)研究[D];中國科學院研究生院（計算技術研究所）;2006年

9 尚慶紅;半分布式系統(tǒng)資源發(fā)現(xiàn)與資源分配研究[D];電子科技大學;2013年

10 田耘;分布式系統(tǒng)中的壓縮感知研究[D];北京郵電大學;2015年

相關碩士學位論文 前10條

1 鄭帥;基于發(fā)布/訂閱的分布式系統(tǒng)信息傳輸性能預測方法[D];哈爾濱工業(yè)大學;2018年

2 沈軒;基于DDS分布式系統(tǒng)的評估指標體系研究及應用[D];東南大學;2018年

3 周瀅瀅;面向發(fā)布/訂閱分布式系統(tǒng)測試的在線錯誤定位技術研究[D];東南大學;2018年

4 張峰;基于高實時分布式網(wǎng)絡的爬蟲軟件設計與實現(xiàn)[D];浙江大學;2018年

5 代長波;分布式系統(tǒng)自適應故障檢測技術研究[D];浙江大學;2017年

6 馮詩淳;大規(guī)模分布式系統(tǒng)監(jiān)控技術研究與應用[D];浙江大學;2017年

7 何騰蛟;分布式系統(tǒng)測試模型與框架的研究與應用[D];電子科技大學;2009年

8 任偉;Social Networks對恢復大規(guī)模分布式系統(tǒng)的性能影響研究[D];電子科技大學;2010年

9 許帥;分布式系統(tǒng)中的信息流控制模型的研究[D];上海交通大學;2011年

10 向永歆;無線家庭媒體網(wǎng)絡分布式系統(tǒng)的設計與實現(xiàn)[D];華中科技大學;2007年

本文編號：2891142