中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
带实时的传值与移动系统研究
作者: 陈靖
答辩日期: 2003
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 实时系统 ; 数据传送 ; 移动计算 ; 进程代数 ; 互模拟 ; 可达性 ; 模型检测
其他题名: Study of Real-time Value-passing and Real-time Mobile Systems
摘要: 实时系统是一种要求反应或计算必须在规定时间内发生的系统。由于这些系统在工业及国防领域有着重要而广泛的应用,因此对这些系统进行形式化分析也成为近年来的一个研究热点。随着社会的发展,尤其是网络的普及和应用,包括通讯协议和控制系统在内的越来越多的软件都以并发的方式运行,我们研究的就是这类带并发的实时系统。在对并发系统的研究中,传值和移动计算分别是两个不同的研究热点。在现有文献中,虽然对一些传统的基本并发系统都进行了实时扩充,得到了如Timed CCS,.Timed CSP等实时演算,但尚未有能刻划实时传值系统的演算,而对移动演算,虽然有少数对7r演算进行实时扩充的工作,但其语义是基于离散时间域的,并不能刻划时间在实数域上连续增长(流逝)等精确行为。本文的研究工作主要由对实时传值系统和实时移动系统的建模和分析组成。对于实时传值系统,本文的研究从计算模型与语义理论、分析与验证算法以及支持工具三个层面展开。在计算模型与语义理论方面着重探讨了带并发性的实时传值模型,定义了一个新的计算模型一时间符号迁移图(Timed Symbolic Transition GraPh),并建立了合适的语义理论。在分析与验证算法的设计方面,在新的计算模型基础上,我们分析了实时传值进程间各种不同互模拟的特点以及判定方法;尤其针对时间互模拟,根据符号互模拟的思想,本文给出了一个时间符号迁移图上的判定算法并证明了算法的正确性。在模型检测的算法方面,本文首先给出了时间符号迁移图上的一个可达性分析算法,随后还定义了能刻划更复杂性质的实时谓词拼演算并给出了检测这些性质的相应模型检测算法。为了有效地对连续时间进行表示和操作,本文针对通常使用的数据结构的范式化过程中出现的问题提出了一种新的信息消冗算法。在给出基本算法的基础上,我们构造了相应的验证工具-RealM,并在本文中给出了对限时重传协议进行的实例分析。对于实时移动系统,本文对7T演算进行了实时扩充,给出了实时万演算的语法和语义,并定义了该演算上的各种互模拟关系,以及相关的性质。本文不但证明了经典万演算的多数性质在新的模型下得到保持,还进一步给出了与时间有关的一些新的等式公理。最后,本文对实时π演算的一个有穷子集上的强实互模拟以及强互模拟均给出了完备的公理化结果。
英文摘要: Real-time systems are computational systems which must respond to externally generated stimuli or inputs within specified time limits. With extensive applications in industry and defence, formal analysis of real-time systems has been an important research area in recent years. During the last two decades, considerable efforts have been devoted into extending existing process theories with real-time features. However, most of these efforts were focused on so-called basic (or pure) calculi where processes running in parallel can only synchronize on signals rather than transmit messages. As most real-time concurrent systems do involve message-passing or link-passing, there is a need to develop formal models and algorithms which can be applied to real-time message-passing and mobile systems. This is the topic of the thesis. The main work of the thesis consists of modeling and analysing real-time value-passing systems and real-time mobile systems. The first work can be divided into three parts: computation model and semantics theory, algorithms for analysing and verification, as well as a tool for computer aided verification. First, a new model, TSTG (Timed Symbolic Transition Graph) is presented along with its semantics theory. An algorithm deciding timed bisimulation is developed based upon the idea of symbolic bisimulations. Model checking algorithms has played an very important role in verifying systems. So we present an algorithm based on reachability analysis, and a more complex one which uses a stronger temporal logic (timed predicateμcalculus) and can verify more properties. To efficiently represent and manipulate continuous time semantics, an optimization method for eliminating redundant information is developed. Based on the above research, a tool named RealM is implemented and a case analysis of a real-time protocol is presented. Another work is on real-time mobile systems. A new computation model, Timed calculus is presented, which is a real-time extension of the standard π calculus on continuous time domain. The syntax and the semantics of the calculus are given, and properties of timed bisimulations are examined. Finally, the strong ground bisimulation and strong bisimulation over a finite subset of Timed ix are completely axiomatized.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6808
Appears in Collections:中科院软件所

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

Recommended Citation:
陈靖. 带实时的传值与移动系统研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2003-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[陈靖]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[陈靖]‘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