导读:本文包含了移动演算论文开题报告文献综述及选题提纲参考文献，主要关键词:移动分布式系统,进程演算,形式语义学,程序统一理论
移动演算论文文献综述
谢宛玲[1]（2019）在《移动分布式系统的进程演算BigrTiMo及其形式语义研究》一文中研究指出移动分布式系统中的计算描述的是如何向分布在不同位置的用户提供高质量的信息服务,目前已经被广泛地应用于教育科研、国防军事、交通运输和航空航天等领域。移动计算的移动性和本身所处的环境会显着地影响通信质量,可能会导致原本可以通信的双方无法继续通信。因此如何刻画移动计算的特征和环境从而提高服务质量成为重要的研究点。本文使用形式化方法对移动分布式系统开展了研究,提出了移动分布式系统的进程演算BigrTiMo。和现有的演算相比,我们的演算不但捕捉了移动计算的移动性,还刻画了移动计算的空间结构和时间特性。在形式语义学的指导下,本文研究了BigrTiMo演算的操作语义,并在Maude工具中对语义规则进行了实现。在图灵奖获得者C.A.R.Hoare教授和何积丰院士所提出的程序统一理论的指导下,本文研究了BigrTiMo演算的指称语义、代数语义和语义连接理论,集中研究了从代数语义生成操作语义和指称语义。基于霍尔逻辑,本文研究了BigrTiMo演算的证明系统,该证明系统用于验证程序的正确性。本文的主要内容和贡献包括如下几点:·本文提出了移动分布式系统的进程演算BigrTiMo,该演算结合了rTiMo演算和图灵奖获得者Robin Milner教授的偶图模型。rTiMo演算只可以建模局部通信,为了支持远程通信的建模,我们在rTiMo演算的基础上引入了偶图模型,从而提出了BigrTiMo演算。我们的演算不但可以描述移动性,还可以刻画空间结构和时间特性。·本文研究了BigrTiMo演算的语义模型,包括操作语义、指称语义、代数语义和证明系统。操作语义直观地刻画了程序运行的过程。基于重写引擎Maude,我们对演算的操作语义进行了重写并对实际生活案例进行了仿真和验证。指称语义基于数学理论,以更加抽象的方式刻画了程序的行为。代数语义由一系列的代数规则组成,为了支持代数并发规则的研究,我们引入了卫兵选择的概念。基于指称语义,我们证明了代数规则的正确性。证明系统是由一系列的证明规则组成,用于验证程序的正确性。我们证明了证明系统的可靠性并通过案例展示了证明系统的应用。·本文研究了语义连接,主要研究了从代数语义生成操作语义和指称语义。为了支持语义的生成,我们引入了首规范型的概念,基于首规范型,我们定义了生成策略,从而生成了变迁系统(操作语义)和指称语义。我们证明了变迁系统和生成策略的等价性,揭示了操作语义的正确性和完备性。(本文来源于《华东师范大学》期刊2019-04-01）
高娟,丁志义[2]（2016）在《基于Pi-演算的移动自助服务系统缴费流程的建模与验证》一文中研究指出在应用Pi-演算对移动自助服务系统的缴费流程建模时,采用自顶向下的方法,首先建立了顶层的缴费流程模型,然后将主要的活动逐层细化,最终得到移动自助服务系统缴费流程的完整模型,同时在Pi-演算专业仿真软件工具MWB中验证了该模型的正确性。(本文来源于《宁夏工程技术》期刊2016年02期）
高娟[3]（2016）在《基于Pi-演算的移动自助服务系统的建模与验证》一文中研究指出移动自助服务系统通过有线或无线网络实现了对其自助服务终端的远程监视和控制,方便公司内部管理,并且为用户提供了方便的途径完成缴费和其他基础业务。由于系统的复杂性,对于系统的分析和验证显得尤为重要,这时就需要建立一种精确的可模拟系统动态运行的模型。在移动自助服务系统中,与进程交互的外部环境也在动态地改变,具有随机性、动态性、计算的复杂性和应用的广泛性。1992年,英国着名的科学家和图灵奖获得者Robin Miler建立和提出了Pi-演算理论。Pi-演算可以描述结构不断变化的分布式并发系统,是一种新的通信建模方法。所以本文采用了Pi-演算形式化方法为系统建模。本文在对移动自助服务系统的缴费流程进行建模时,采用自顶向下的建模方法,首先在分析系统缴费流程的基础上,提取出其中的主要活动模块,建立顶层的Pi-演算模型；然后细化这些模块,详细地分析每一个模块包含的细节活动,继而得出完整的Pi-演算模型；最后使用Pi-演算的形式化验证工具MWB验证了模型的正确性(如有无死锁),而且用step命令模拟了自助服务系统平台的交互运行情况,可以看出它满足了预期设计的要求。移动自助服务系统所采用的通信协议是TCP/IP协议；本文为了达到对协议进行安全性验证的目的,主要分析了其中的传输控制协议TCP。在分析TCP协议中的数据报格式、连接的建立和释放以及快速重传算法的基础上,对TCP建立连接时采取的叁次握手协议建立了Pi-演算模型,并在MWB工具中用step命令模拟了叁次握手的动态运行,从理论的角度分析了快速重传机制在建立TCP连接时的应用,给人们控制进程带来很多的益处。本文为系统的缴费流程建立了精确的Pi-演算模型,同时也用Pi-演算理论分析了TCP建立连接的叁次握手协议,对系统达成了一致的理解,奠定了系统的分析和改进。(本文来源于《宁夏大学》期刊2016-05-01）
丛新宇,虞慧群[4]（2015）在《基于安全灰箱演算的物联网移动性建模验证》一文中研究指出物联网的建模和验证是物联网研究的一个重要领域。由于集成了物理进程,物联网表现出传统软件系统所不具备的物理特性。这些性质作为物联网系统中必不可少的一部分,必须在物联网模型中进行描述。移动性作为一种物理属性,能够描述物联网中物理实体的移动以及信息的流动,本文对物联网的移动性进行研究,提出了一种基于安全灰箱演算的物联网模型,并且使用灰箱逻辑对其进行分析验证。该方法能够对物联网的移动性进行描述分析,适用于具有移动特征的物联网应用。以欧洲火车控制系统(ETCS)为例,验证了本文建模和验证方法的可行性。(本文来源于《华东理工大学学报(自然科学版)》期刊2015年03期）
罗玲,段振华[5]（2014）在《扩展π演算对时间相关移动并发系统的建模与推演》一文中研究指出针对π演算难于对时间相关移动并发系统进行建模和推演,提出了一种采用扩展π演算p-π对时间相关移动并发系统进行形式化建模与推演的方法。该方法首先采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作算子将子进程进行复合,然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径,最后基于上述迁移系统和执行路径完成对系统性质的推演。对移动车辆控制系统的分析表明,所提方法可对时间相关移动并发系统进行有效建模和推演,保证时间相关移动并发系统的可靠性。(本文来源于《西安交通大学学报》期刊2014年09期）
王梦莹[6]（2013）在《移动自组网络的时间演算》一文中研究指出作为一种由可移动的无线节点组成的复杂分布式系统,移动自组网络具有如下叁方面的特点：(1)区域广播,即节点广播只能覆盖该节点传输信元范围内的有限邻居节点；(2)节点移动,指节点可以任意改变自身的位置,在网络内自由移动；(3)通信冲突,无线频道的单工性,使得发送节点无法及时检测到通信冲突,同时,节点的移动更加剧了通信冲突问题的严重性。因此,本文提出了TCMN时间演算语言,旨在同时刻画移动自组网络的这叁方面特性。首先,我们定义了TCMN时间演算语言中的各种操作算子,并为之提供了相应的规约语义和标签转换语义两种不同的操作语义。其中,前者只关注系统的内部动作,因此便于读者理解：而后者除此之外,还会兼顾系统与周围环境的交互行为,所以能够提供强有力的证明技巧。然后,我们又根据移动自组网络的特点,提出了规范网络的概念,定义了正确的网络结构所必须满足的特性：节点唯一性、位置唯一性、曝光一致性和通信一致性。并在此基础上,证明了规约语义和标签转换语义的一致性,以此来表明我们提出的标签转换语义的正确性。此外,TCMN时间演算语言享有叁个令人非常满意的时间特性：(i)时间确定性,即随着全局时钟的不断向前流逝,网络每次演变为的新状态都是确定的；(ii)最大前进性,即消息广播事件不能够被延迟,必须立即执行；(iii)耐心等待性,即只有当网络中的所有瞬时动作,如启动消息传输,都执行结束时,全局时钟才能够流转到下一个时钟周期。最后,我们通过学习并建模了移动自组网络中的若干MAC协议,一方面展示了TCMN时间演算语言丰富的表达能力和完备的操作语义,另一方面也旨在说明这些协议在消除通信冲突方面的有效性或者指出其不足之处。(本文来源于《华东师范大学》期刊2013-04-01）
喻莉,姜烈,罗晶晶,张婕[7]（2012）在《基于跨层网络演算模型的无线网络移动性能分析》一文中研究指出为了研究终端移动对无线网络服务质量(QoS)的影响,该文建立了跨层网络演算模型来计算通信终端处于不同移动速度下无线网络的延时积压性能参数。该模型的建立结合了跨层分析思想和网络演算理论,将无线网络中网络层、链路层及物理层等层次的特性映射为一系列网络演算模块的串联。基于构造的模型应用网络演算能够方便地推导出终端处于不同移动速度下无线网络的服务曲线,进而计算出网络的延时积压性能。仿真结果表明,构造的跨层网络演算模型可以准确地分析终端在不同移动速度下无线网络的延时积压性能。(本文来源于《电子与信息学报》期刊2012年01期）
陈江,林荣德[8]（2011）在《具有行为观察的移动界程演算空间逻辑》一文中研究指出界程逻辑中的并发模态副词是观察进程交互行为的关键因素之一,但引入并发模态副词又会导致模型检测的不可判定性.针对这一问题,提出了可判定的、描述移动界程演算进程的空间结构和行为性质的应用界程逻辑.该逻辑定义了空间模态词和行为模态词来直接观察移动进程的空间性质和潜在交互行为性质,并定义了不动点公式来刻画进程的递归性质.为了证明逻辑公式的指称语义的正确性,引入了性质集的概念并证明两者之间的一致性.最后给出了使用应用界程逻辑公式来描述一个资源传输系统在时间和空间上的行为性质的实例.(本文来源于《南京师范大学学报(工程技术版)》期刊2011年04期）
高超[9]（2011）在《基于Pi-演算的第叁代移动通信服务的形式化建模与研究》一文中研究指出当今,伴随国际互联网在全球范围的广泛普及和应用,Web服务组合也在不断地变化发展。Web服务具有松散耦合性、平台无关性等特性,能够提供兼容已有系统的跨平台分布式应用,提供更为多样的服务。同时,移动通信在发展过程中,需要解决如何满足用户不断增长的需求、统一服务标准等方面的问题。当前的第叁代移动通信已经呈现出IP化的趋势,本文用Web服务的形式表示移动通信,将第叁代移动通信和Web服务结合起来,以研究解决以上移动通信当前所面临问题的方法。在研究过程中,本文采用Pi-演算作为建模工具,利用Pi-演算和Web服务之间的联系,发挥Pi-演算特有的优势,合理地建立了移动通信的Web服务模型,并且进行了严格的验证。本文首先介绍了移动通信、Pi-演算及Web服务的相关理论,并对第叁代移动通信核心网的IP多媒体子系统中有代表性的移动通信过程进行了分析。通过研究具有代表性的移动通信过程,提出了一种适合移动通信过程的消息机制,利用Pi-演算完成了以上移动通信过程Web服务形式的建模。根据建模工作总结出一种适合本文研究模型的基于Pi-演算的Web服务描述方法,以服务为单位,定义了基于Pi-演算的第叁代移动通信核心网的Web服务。最后,本文利用Pi-演算的自动化工具——MWB对所建模型进行了正确性验证,并且利用Web服务开发工具对前文中在服务方面更具代表性的模型进行了模拟实现,完整实现了其功能,最终完善了前文的研究。(本文来源于《吉林大学》期刊2011-04-01）
乔爽,张春城,顾宏[10]（2010）在《基于时间π-演算的移动商务过程建模》一文中研究指出在总结无线技术对商务活动的影响的基础上,针对信息交互频繁、不确定环境下的过程结构动态变化、局部自治等柔性特征,采用时间π-演算为移动商务过程建模,目的在于便于分析时间绩效改进。然后,具体指出了π-演算和移动商务过程的对应关系,构建了具有共性的选择过程组件,以及在时间方面扩展了π-演算。最后,用无线自动售货机系统的物流配送过程实例,证明了方法的有效性。(本文来源于《管理学报》期刊2010年06期）
移动演算论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
在应用Pi-演算对移动自助服务系统的缴费流程建模时,采用自顶向下的方法,首先建立了顶层的缴费流程模型,然后将主要的活动逐层细化,最终得到移动自助服务系统缴费流程的完整模型,同时在Pi-演算专业仿真软件工具MWB中验证了该模型的正确性。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
移动演算论文参考文献
[1].谢宛玲.移动分布式系统的进程演算BigrTiMo及其形式语义研究[D].华东师范大学.2019
[2].高娟,丁志义.基于Pi-演算的移动自助服务系统缴费流程的建模与验证[J].宁夏工程技术.2016
[3].高娟.基于Pi-演算的移动自助服务系统的建模与验证[D].宁夏大学.2016
[4].丛新宇,虞慧群.基于安全灰箱演算的物联网移动性建模验证[J].华东理工大学学报(自然科学版).2015
[5].罗玲,段振华.扩展π演算对时间相关移动并发系统的建模与推演[J].西安交通大学学报.2014
[6].王梦莹.移动自组网络的时间演算[D].华东师范大学.2013
[7].喻莉,姜烈,罗晶晶,张婕.基于跨层网络演算模型的无线网络移动性能分析[J].电子与信息学报.2012
[8].陈江,林荣德.具有行为观察的移动界程演算空间逻辑[J].南京师范大学学报(工程技术版).2011
[9].高超.基于Pi-演算的第叁代移动通信服务的形式化建模与研究[D].吉林大学.2011
[10].乔爽,张春城,顾宏.基于时间π-演算的移动商务过程建模[J].管理学报.2010