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

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

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

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

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

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

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

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

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

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

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

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

相關(guān)博士學(xué)位論文 前10條

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

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

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

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

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

6 鄧超;面向Agent的智能化分布式計(jì)算及其應(yīng)用研究[D];浙江大學(xué);2005年

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

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

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

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

相關(guān)碩士學(xué)位論文 前10條

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

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

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

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

5 代長(zhǎng)波;分布式系統(tǒng)自適應(yīng)故障檢測(cè)技術(shù)研究[D];浙江大學(xué);2017年

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

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

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

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

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

本文編號(hào)：2891142