【摘 要】
：
移动分布式系统中的计算描述的是如何向分布在不同位置的用户提供高质量的信息服务,目前已经被广泛地应用于教育科研、国防军事、交通运输和航空航天等领域。移动计算的移动性和本身所处的环境会显著地影响通信质量,可能会导致原本可以通信的双方无法继续通信。因此如何刻画移动计算的特征和环境从而提高服务质量成为重要的研究点。本文使用形式化方法对移动分布式系统开展了研究,提出了移动分布式系统的进程演算BigrTiMo
论文部分内容阅读
移动分布式系统中的计算描述的是如何向分布在不同位置的用户提供高质量的信息服务,目前已经被广泛地应用于教育科研、国防军事、交通运输和航空航天等领域。移动计算的移动性和本身所处的环境会显著地影响通信质量,可能会导致原本可以通信的双方无法继续通信。因此如何刻画移动计算的特征和环境从而提高服务质量成为重要的研究点。本文使用形式化方法对移动分布式系统开展了研究,提出了移动分布式系统的进程演算BigrTiMo。和现有的演算相比,我们的演算不但捕捉了移动计算的移动性,还刻画了移动计算的空间结构和时间特性。在形式语义学的指导下,本文研究了BigrTiMo演算的操作语义,并在Maude工具中对语义规则进行了实现。在图灵奖获得者C.A.R.Hoare教授和何积丰院士所提出的程序统一理论的指导下,本文研究了BigrTiMo演算的指称语义、代数语义和语义连接理论,集中研究了从代数语义生成操作语义和指称语义。基于霍尔逻辑,本文研究了BigrTiMo演算的证明系统,该证明系统用于验证程序的正确性。本文的主要内容和贡献包括如下几点:·本文提出了移动分布式系统的进程演算BigrTiMo,该演算结合了rTiMo演算和图灵奖获得者Robin Milner教授的偶图模型。rTiMo演算只可以建模局部通信,为了支持远程通信的建模,我们在rTiMo演算的基础上引入了偶图模型,从而提出了BigrTiMo演算。我们的演算不但可以描述移动性,还可以刻画空间结构和时间特性。·本文研究了BigrTiMo演算的语义模型,包括操作语义、指称语义、代数语义和证明系统。操作语义直观地刻画了程序运行的过程。基于重写引擎Maude,我们对演算的操作语义进行了重写并对实际生活案例进行了仿真和验证。指称语义基于数学理论,以更加抽象的方式刻画了程序的行为。代数语义由一系列的代数规则组成,为了支持代数并发规则的研究,我们引入了卫兵选择的概念。基于指称语义,我们证明了代数规则的正确性。证明系统是由一系列的证明规则组成,用于验证程序的正确性。我们证明了证明系统的可靠性并通过案例展示了证明系统的应用。·本文研究了语义连接,主要研究了从代数语义生成操作语义和指称语义。为了支持语义的生成,我们引入了首规范型的概念,基于首规范型,我们定义了生成策略,从而生成了变迁系统（操作语义）和指称语义。我们证明了变迁系统和生成策略的等价性,揭示了操作语义的正确性和完备性。
其他文献
基因水平转移是一种能在不同物种间进行遗传信息交流的遗传方式。尽管突变和有性繁殖是真核生物产生变异的主要来源,但由水平转移机制获得的转移基因在真核生物中可具有重要的生物学功能。由苔类植物门、藓类植物门和角苔植物门组成的苔藓植物,是植物从水生过渡到陆生生活的关键类群之一,在绿色植物的演化历史中具有重要的进化地位。苔藓植物除了可附生在其它陆地植物的叶片和树干上,还能与细菌和真菌,特别是蓝细菌等微生物共生
基因组稳定性的维持对细胞存活和增殖至关重要。基因毒药物（如传统化疗药物）诱发细胞中DNA双链断裂（DSBs）被广泛用于临床肿瘤治疗。然而,发生DSBs的细胞会启动一系列复杂的DNA修复机制来应对DNA损伤,维持细胞基因组的相对稳定,这一过程即DNA损伤应答（DDR）。在DDR发生过程中,细胞内绝大多数基因表达下调,而参与DDR的众多因子能有选择地逃避DNA损伤介导的转录抑制,其mRNA稳定性明显增
已有的关于权力感与决策的相关研究,主要运用接近-抑制理论来解释相关结果,更多关注权力感高低维度对接近和抑制行为的影响,较少关注权力动机的高低及权力感的稳定性维度在其中所起的作用,且多数研究偏向于探讨收益情境下的接近行为,较少探讨损失情境下的抑制行为。特别是,关于权力感何以会影响和改变个体的接近和抑制行为,尚不清楚。本研究试图从风险偏好的视角入手,以实际工作中不同层级的领导干部群体为被试,采用收益损
加纳沃尔特河项目是20世纪60年代非洲一个具有重要影响的国际工程,其发展历程颇为漫长和复杂。自澳大利亚人艾伯特·凯特森在1915年提出沃尔特河项目构想后,吸引了很多私人公司的积极参与,其中又以南非工程师邓肯·罗斯领导下的西非铝业有限公司为首,同时也引起了英国及其黄金海岸殖民地政府的高度关注,他们推动着沃尔特河项目的早期发展。1953年,黄金海岸殖民地政府建立了以罗伯特·杰克逊为主席的沃尔特河项目筹
既有上博簡字跡研究已經取得了很好的成績,但在方法上,如何定量,以及如何合理選定用於字跡比較的典型字符等方面尚有進一步提升的空間,例如,列舉以下7個“典型字”論證《弟子問》與《君子為禮》2篇文獻的“文字書寫軌跡”具有同一性:“則、爲、者、遊、贛、而、富”。通過窮盡性調查,我們發現,“者、遊、富”《君子為禮》篇僅1見;“爲”《君子為禮》篇僅2見;“贛”《弟子問》篇僅2見,這些使用頻率較低的“典型字”,
可变剪接普遍存在于真核生物中,是基因表达调控的重要环节,通过外显子的不同组合可产生一系列差异转录本,在极大程度上丰富了生物体的转录组和蛋白质组多样性。同时,异常的可变剪接也将直接导致机体生理功能的紊乱。因此,可变剪接事件对于生物体正常生理功能的实现是至关重要的。唐氏综合征细胞黏附分子（Dscam）是可变剪接的代表性基因,在果蝇（D.melanogaster）中可潜在产生38,016种可变剪接异构体
本文综合新课程物理教材的胡克定律实验设计思想和创新的实验方法,对胡克定律的实验进行了改进,重点介绍了设计的弹簧弹力与形变量关系探究仪,该演示仪既可以精确地得出胡克定律,又可以对弹簧的劲度系数进行进一步的探究。
近几年来,同时基于光纤传输和星地传输的量子保密通信发展迅猛,世界主要国家高度关注量子信息技术发展,甚至上升为国家战略。早在2013年,我国就前瞻部署了世界首条远距离量子保密通信“京沪干线”,率先开展了相关技术的应用示范并取得系列宝贵经验。随着量子信息技术的不断发展,量子信息最常用的载体——通信波段红外光子的单光子探测技术也被推动向前。然而当前应用较广的近红外单光子探测器如InGaAs APD和SN
Ⅰ-Ⅱ-Ⅳ-Ⅵ族（其中Ⅰ=Cu或Ag;Ⅱ=Zn、Cd、Ni、Co、Fe或Mn;Ⅳ=Si、Ge或Sn;VⅠ=S、Se或Te等）多元化合物具有组成元素丰富、价格低廉、环境友好等优点以及优异的电学、光学、磁学和热学等物理性质,从而在太阳能光伏、热电、光催化、非线性光学等领域具有重要的潜在应用价值。该类材料的晶体结构通常遵循八隅体规则,其中阳离子具有相同的占位,随成分的变化可形成多种不同的有序结构。由于这
目的 分析切开根治术对低位肛周脓肿患者创面愈合速度、术后疼痛及肛门功能的影响。方法 选取本院2019年6月至2021年6月收治的106例低位肛周脓肿患者作为研究对象，根据治疗方案的差异分为研究组和对照组，各组53例。研究组患者接受切开根治术，对照组接受传统分期治疗（切开引流后行Ⅱ期肛瘘术）。对比两组创面愈合时间、术后首次排气时间和首次排便时间，比较两组术后肛门疼痛情况，以Starck评分和Wexn