移动分布式系统的进程演算BigrTiMo及其形式语义研究

发布时间：2020-11-20 07:16

　　 移动分布式系统中的计算描述的是如何向分布在不同位置的用户提供高质量的信息服务,目前已经被广泛地应用于教育科研、国防军事、交通运输和航空航天等领域。移动计算的移动性和本身所处的环境会显著地影响通信质量,可能会导致原本可以通信的双方无法继续通信。因此如何刻画移动计算的特征和环境从而提高服务质量成为重要的研究点。本文使用形式化方法对移动分布式系统开展了研究,提出了移动分布式系统的进程演算BigrTiMo。和现有的演算相比,我们的演算不但捕捉了移动计算的移动性,还刻画了移动计算的空间结构和时间特性。在形式语义学的指导下,本文研究了BigrTiMo演算的操作语义,并在Maude工具中对语义规则进行了实现。在图灵奖获得者C.A.R.Hoare教授和何积丰院士所提出的程序统一理论的指导下,本文研究了BigrTiMo演算的指称语义、代数语义和语义连接理论,集中研究了从代数语义生成操作语义和指称语义。基于霍尔逻辑,本文研究了BigrTiMo演算的证明系统,该证明系统用于验证程序的正确性。本文的主要内容和贡献包括如下几点:·本文提出了移动分布式系统的进程演算BigrTiMo,该演算结合了rTiMo演算和图灵奖获得者Robin Milner教授的偶图模型。rTiMo演算只可以建模局部通信,为了支持远程通信的建模,我们在rTiMo演算的基础上引入了偶图模型,从而提出了BigrTiMo演算。我们的演算不但可以描述移动性,还可以刻画空间结构和时间特性。·本文研究了BigrTiMo演算的语义模型,包括操作语义、指称语义、代数语义和证明系统。操作语义直观地刻画了程序运行的过程。基于重写引擎Maude,我们对演算的操作语义进行了重写并对实际生活案例进行了仿真和验证。指称语义基于数学理论,以更加抽象的方式刻画了程序的行为。代数语义由一系列的代数规则组成,为了支持代数并发规则的研究,我们引入了卫兵选择的概念。基于指称语义,我们证明了代数规则的正确性。证明系统是由一系列的证明规则组成,用于验证程序的正确性。我们证明了证明系统的可靠性并通过案例展示了证明系统的应用。·本文研究了语义连接,主要研究了从代数语义生成操作语义和指称语义。为了支持语义的生成,我们引入了首规范型的概念,基于首规范型,我们定义了生成策略,从而生成了变迁系统(操作语义)和指称语义。我们证明了变迁系统和生成策略的等价性,揭示了操作语义的正确性和完备性。
【学位单位】：华东师范大学
【学位级别】：博士
【学位年份】：2019
【中图分类】：TN929.5
【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 研究背景和动机
    1.2 研究现状和相关工作
    1.3 本文的主要工作和架构
第二章 基础理论和指导方法
    2.1 进程演算
    2.2 rTiMo演算的语法
    2.3 偶图模型
    2.4 形式语义学
    2.5 程序统一理论
    2.6 Maude概述
第三章 移动分布式系统的进程演算BigrTiMo
    3.1 BigrTiMo演算的语法
    3.2 BigrTiMo演算的操作语义
    3.3 基于Maude的仿真与验证
    3.4 本章小结
第四章 BigrTiMo演算的指称语义
    4.1 语义模型与健康条件
    4.2 基本命令的指称语义
    4.3 卫兵选择的指称语义
    4.4 并发组合的指称语义
    4.5 本章小结
第五章 BigrTiMo演算的代数语义及其语义连接
    5.1 BigrTiMo演算的代数语义
    5.2 首规范型
    5.3 代数语义和操作语义之间的连接
    5.4 代数语义和指称语义之间的连接
    5.5 本章小结
第六章 BigrTiMo演算的证明系统
    6.1 描述规范
    6.2 证明规则
    6.3 证明系统的可靠性
    6.4 证明系统的应用案例
    6.5 本章小结
第七章 总结与展望
    7.1 本文工作总结
    7.2 后续工作展望
参考文献
致谢
攻读博士学位期间发表论文和科研情况

【相似文献】

相关期刊论文 前10条

1 沈涛;;分布式系统动目标防御[J];通信对抗;2016年04期

2 黄炜耀;;分布式系统中的周期性事件实现研究[J];信息通信;2017年09期

3 ;分布式系统概念与设计[J];计算机教育;2013年08期

4 George Coulouri;Jean Dollimore;Tim Kindberg;Gordon Blair;;分布式系统概念与设计[J];计算机教育;2013年10期

5 George Coulouris;Jean Dollimore;Tim Kindberg;Gordon Blair;;分布式系统概念与设计[J];计算机教育;2013年12期

6 姜冬;王慧强;冯光升;吕宏武;林俊宇;;基于模糊层次化评估的分布式系统自毁感知方法及应用[J];小型微型计算机系统;2012年04期

7 陈建英;杨宪泽;张楠;;面向大规模分布式系统的多级缓存信息结构研究[J];西南民族大学学报(自然科学版);2012年03期

8 况晓辉;赵刚;温研;许飞;苗青;;大规模分布式系统脆弱性分析框架研究[J];计算机科学;2012年06期

9 赵刚;赵金晶;况晓辉;郑纬民;;大规模分布式系统实体交互脆弱性分析方法[J];计算机工程与应用;2011年18期

10 杜文晟;;浅论分布式系统中间件的安全[J];湖北师范学院学报(自然科学版);2010年01期

相关博士学位论文 前10条

1 谢宛玲;移动分布式系统的进程演算BigrTiMo及其形式语义研究[D];华东师范大学;2019年

2 梅晶;并行分布式系统中的节能调度策略与算法研究[D];湖南大学;2015年

3 童钊;基于计算智能的并行分布式系统任务调度算法研究[D];湖南大学;2014年

4 李晋国;分布式系统中的安全协议研究[D];湖南大学;2014年

5 彭舰;基于CORBA的分布式系统中实时—容错性的研究——分布式系统中动态调度的设计与实现[D];电子科技大学;2004年

6 邓超;面向Agent的智能化分布式计算及其应用研究[D];浙江大学;2005年

7 吕毅;证明和测试分布式系统的功能正确性[D];中国科学院研究生院（计算技术研究所）;2004年

8 龚奕利;分布式环境中的资源发现研究[D];中国科学院研究生院（计算技术研究所）;2006年

9 尚庆红;半分布式系统资源发现与资源分配研究[D];电子科技大学;2013年

10 田耘;分布式系统中的压缩感知研究[D];北京邮电大学;2015年

相关硕士学位论文 前10条

1 郑帅;基于发布/订阅的分布式系统信息传输性能预测方法[D];哈尔滨工业大学;2018年

2 沈轩;基于DDS分布式系统的评估指标体系研究及应用[D];东南大学;2018年

3 周滢滢;面向发布/订阅分布式系统测试的在线错误定位技术研究[D];东南大学;2018年

4 张峰;基于高实时分布式网络的爬虫软件设计与实现[D];浙江大学;2018年

5 代长波;分布式系统自适应故障检测技术研究[D];浙江大学;2017年

6 冯诗淳;大规模分布式系统监控技术研究与应用[D];浙江大学;2017年

7 何腾蛟;分布式系统测试模型与框架的研究与应用[D];电子科技大学;2009年

8 任伟;Social Networks对恢复大规模分布式系统的性能影响研究[D];电子科技大学;2010年

9 许帅;分布式系统中的信息流控制模型的研究[D];上海交通大学;2011年

10 向永歆;无线家庭媒体网络分布式系统的设计与实现[D];华中科技大学;2007年

本文编号：2891142