中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
分布式系统形式化建模技术研究
作者: 郑红
答辩日期: 2003
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 分布式系统 ; CORBA规范
其他题名: Research on Formal Modeling of Distributed Systems
摘要: 分布式计算经过近年来的迅速发展,已形成多种规范或标准,广泛应用于分布式系统设计和开发。然而,这些工业规范或标准明显缺乏坚实的理论基拙,从而给分布式系统的规格说明、正确性验证、安全性等工作带来诸多不便。对分布式应用软件系统开发者而言,开发跨平台、跨地域的大型分布式系统仍然足一项相当繁重而复杂的任务。OMG提出的CORBA(Common Object Request Broker Architecture,CORBA)作为分布式计算标准,仅仅是规范,而不是实现。形式化方法支持大型复杂的软件系统的形式模拟和验证,它可以将软件系统非形式化规范转化为具有严格语义的形式化描述,从而便于系统设计人员阅读、理解、修改、验证和设计开发。因此,从软件系统的形式模拟与验证到实际的开发应用,形式化方法都起着一个重要的桥梁作用。通过对分布式系统的形式化分析,可以查找出系统设计中的漏洞或缺陷,能够帮助设计者修改和优化系统,使其更规范、有效、合理。形式化方法对分布式计算理论模型研究主要是将涉及分布与并发行为的各种概念形式化,从而给出这些行为的精确定义,避免系统开发人员理解上的二义性,并且为系统开发人员提供可靠的数学工具,用于说明、设计和验证分布式系统的多个方面,如系统运行的正确性、安全性等。显然,开发分布式系统比传统的集中式系统更需要一种精确的数学模型。目前,国内外可用于分布式系统形式描述与验证的形式化方法主要分为四大类:基于模型的方法、基于逻辑方法、基于进程演算的方法,以及基于网络的方法等等。本文在综合分析并比较了它们的应用特点及不足后,以Petri网为形式化工具,研究了基于CORBA分布式系统的建模技术。本文研究工作的主要贡献表现在如下几个方面:(1)从理论上研究并分析了CO邓A对象服务规范与其扩展着色Petri网模型的动态行为一致性。分析表明扩展着色Petri网模型不仅能够清楚描述系统对象的静态行为,同时也能极好地模拟系统分布性和动态性。(2)对于分布式系统的安全性,本文应用标注着色Petri网模拟技术,明确描述和分析了CO邓A分布式系统主体责任、证据等与安全性有关的重要性质,并研究了分布式系统不可否认性的模拟验证技术。(3)用时序Petri网模拟和分析了分布式系统的ACID事务处理,为构建基于CORBA的事务处理系统提供了分析方法。此外,本文综合应用时间Petri网和工作流网的概念,研究并分析了分布式系统工作流的形式化模拟技术和验证方法。
英文摘要: Distributed computing has formed various specifications or standards with its rapid progress in recent years, and can be applied to develop distributed software systems. However, these industry specifications or standards obviously lack solid theory foundation, which causes great inconvenience to distributed software system specification, correctness verification and performance evaluation. It is still a hard and complicated job for the developers to develop a large-scale distributed system CORBA(Common Object Request Broker Architecture,CORBA) is a set of open standards proposed by the OMG in order to promote interoperability between distributed systems, and it is not implementation but only specification. The aim of the formal method is to support the formal simulation and verification of large-scale application systems. Formal methods convert informal specifications into formal description for the purpose that the dynamic behaviors of the modeled systems can be formally described with unambiguous precise definitions, and effective matheniatic tools for the specification, design and verification of parallel and distributed system can also be provided. Therefore, the formal method plays an important role as a bridge between the model simulation, verification of application systems. The formal simulation and analysis of the application system can point out the defects in the system designing and help to modify and enhance the system to make it more sound, effective and reasonable. Formal methods have contributed a lot to the distributed system simulation and analysis. Formal methods over the distributed computing theory model are to formalize all the concepts concerning with the distribution and concurrent behaviors so as to define these accurately and avoid the ambiguity. Because of the inherent distributed nature, transmission delay of the network information, heterogeneous of network platforms, it is obvious that developing a distributed system requires a more accurate mathematics model than the traditional concentrated one. It is necessary to use formal methods to analyze and verify the distributed system so as to provide reliable mathematics tools for the explanation, design and verification of the distributed system, such as the correctness and security of the distributed system. At present, formal methods that can be used to describe and verify in the distributed system model are mainly categorized into four types: methods based on models, methods based on logic, methods based on processing calculus, methods based on networks. This paper illustrates the above methods characteristics and defects, and focus on formal modeling of the CORBA distributed system based on Petri nets. The main contributions of this paper are as follows: ( 1) This paper introduces an extended Colored Petri net to express the behaviors of individual objects, the concurrency between different objects as well as the intra-object concurrency in the context of CORBA, and gives formal specifications of the CORBA Event Service. For the security of the distributed system, the paper applies the Labeled Colored Petri nets to describe and analyze clearly the subjective responsibility and evidence contained in CORBA security service and provides the non-repudiation model based on CORBA security. The paper simulates and analyzes the ACID transaction of distributed system by using the temporal Petri nets, provides an analysis method for building the transaction processing system based on CORBA. In addition, the paper describes and analyzes some issues concerning the workflow with Timed Petri nets and the notions of work flow nets.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6940
Appears in Collections:中科院软件所

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

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