中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
题名:
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.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/5740
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_2003180150F0001Takashi KITAMURA_paper.pdf(881KB)----限制开放-- 联系获取全文

Recommended Citation:
Takashi KITAMURA. Formalization and specification for controlling process modularity in mobile computing[D]. 软件研究所. 中国科学院软件研究所. 2008-06-05.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Takashi KITAMURA]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Takashi KITAMURA]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace