QQ客服 官方微博 反馈留言

题名	Formalization and specification for controlling process modularity in mobile computing
作者	Takashi KITAMURA
学位类别	博士
答辩日期	2008-06-05
授予单位	中国科学院软件研究所
授予地点	软件研究所
关键词	进程代数 Pi演算 分布移动计算 模态逻辑 Mu演算 模型检测
其他题名	Formalization and specification for controlling process modularity in mobile computing
中文摘要	新的计算模式，普适计算和全局计算，正在作为高度分布式和移动计算的计算模式展现出来。这篇论文探讨了在抽象层面上支持这些新型计算模式的适合的形式化基础，关注在进程移动单位上的控制, 以便在分布式与移动计算环境下更好地协调进程的移动性。 论文的第一部分概述了针对分布式、移动计算的现有进程演算模型中的进程移动单元，并且设计了一种在此方面更优、更具弹性的进程框架。为了表示这种进程框架，我们提出了一种新的、针对移动和分布式系统的进程演算,这种进程演算的优点是动态、弹性的控制进程的移动单元；具体的思路就是扩展π- calculus以及其支持分布式和移动性的变体。我们把这种新的演算叫做Modular π-calculus。我们通过这种演算的提出来说明进程框架提供了一种针对移动进程更为合适的协调机制以及编程模型，例如移动的代理和动态组件载入的支持。之后，我们通过讨论互模拟的几种提法来具体说明能够反映演算设计的进程描述的关键，之后我们讨论了它们的具体性质。 本文的第二部分提出了一个对进程模型的行为和性质进行推理的规约框架。首先，提出了一个对Modularπ-calculus中进程的系统性质进行规约的模态逻辑。为了更好的理解该逻辑，文中对由这个逻辑推出的进程等价的特征进行了研究，并且证明了该逻辑的区分能力介于互模拟和结构一致之间。接下来关于这个规约框架的自动化，本文针对该逻辑和Modular π-calculus的有限控制子集，提出了模型检测算法，并且给出了算法正确性的证明。同时文中贯穿了一些实际且直观的例子，以展现本文提出的一组框架即演算、逻辑和模型算法的有效性。
英文摘要	New computing paradigms - ubiquitous computing paradigm and global computing paradigm - are emerging as application paradigms of highly distributed and mobile computing systems. This thesis explores a formal foundation to underpin such new computing paradigms, with a focus on the aspect of control on process mobility units for a better coordination of process mobility in distributed and mobile computing settings. The first part of the thesis develops process calculi which can flexibly and dynamically control process mobility units in process models featured with the notion of process distribution and mobility over flat location space.A simple semantical mechanism to realize dynamic control on process mobility units is considered within process models characterized with the explicit notion of process distribution and mobility over flat location space. And it is formalized in several such process models. Mainly, we discuss the formalization based on Hennessy and Riely's distributed $\pi$-calculus (D$\pi$) \cite{HR98,HR02}, and present a formal calculus, which we may refer to as \textit{Modular $\pi$-calculus}.Main theoretical discussion is on bisimulation relations of the process calculi we propose. Several notions of bisimilarity are designed to clarify the criteria of process specification in the process calculi, and properties on them are investigated. The second part of the thesis investigates specification and verification methods to specify and verify system properties in processes of Modular $\pi$-calculus. First, a modal logic is proposed to specify system properties for processes in Modular $\pi$-calculus. The logic is designed as a spatial logic to observe spatial as well as temporal properties of systems, in order to specify interesting properties for the systems. And also it is designed as a predicate-based modal $\mu$-calculus to bring a clean and simple semantics. As a property of the logic, characterization of the process equivalence the logic induces is investigated; and it is shown that the distinguishing power of the logic lies between bisimilarity and structural congruence. Then, model checking problems are examined; consequently, a model checking algorithm for the logic over a finite-control subset of Modular $\pi$-calculus is presented, and its correctness proved. Practical and intuitive examples are scattered throughout the thesis to illustrate the significance and benefits of the theory and techniques developed in the thesis, such as the modeling, specification and verification techniques.
语种	中文
公开日期	2011-03-17
页码	118
内容类型	学位论文
源URL	[http://124.16.136.157/handle/311060/5740]
专题	软件研究所_计算机科学国家重点实验室 _学位论文
推荐引用方式 GB/T 7714	Takashi KITAMURA. Formalization and specification for controlling process modularity in mobile computing[D]. 软件研究所. 中国科学院软件研究所. 2008.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。