中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
形式化分析方法在OnceAS设计和实现中的应用
作者: 李彦
答辩日期: 2006-06-15
授予单位: 中国科学院软件研究所
授予地点: 软件研究所
学位: 博士
关键词: 应用服务器 ; J2EE ; 模型检查 ; 正确性
摘要: 基于J2EE规范的Web应用服务器作为分布式系统运行时的基础支撑软件,在向客户提供全面的功能性支持的同时,也需要给出优秀的可靠性与兼容性的保障。这就对应用服务器实现的正确性提出了很高的要求。但是应用服务器的正确性受到了很多因素的威胁,例如J2EE规范的中可能的二义性和不完备性,应用服务器的设计与实现的复杂性和并发性。然而,无论是从完备性或是准确性的角度出发,传统的测试方法并不能完善地解决这些问题。在本文中,我们尝试了使用形式化分析的方法应用到OnceAS2.0中一些关键模块的设计与实现中去,验证了它们的正确性。 本文首先以EJB2.1规范中的Timer Service为例,研究了一种基于模型检查技术导出J2EE中间件设计方法。我们从非形式化的J2EE规范出发,提出Timer Service的形式化模型,定义了Timer Service的行为;然后使用模型检查工具SPIN对模型进行分析与验证,不仅证明了模型符合规范要求,而且发现并修正了规范中不严格的描述带来的缺陷。之后,我们以该模型为基础导出了Timer Service的一种设计方案。这种设计的静态结构和系统行为都经过了严格的形式化分析,因而较那些直接以J2EE规范为蓝本提出的系统设计更加严格可靠。 然而,验证系统正确性的最直接的方法是证明系统的实现满足系统的需求。因此本文还以OnceAS2.0中JDBC数据库连接池为例,进一步探讨了如何在Java代码级使用形式化分析技术验证系统的正确性。我们将数据库连接池模块从OnceAS中独立出来并进行化简,使用Bandera模型检查环境验证了连接池的实现并发现了其中的问题,以最直接的方式提升了系统的可靠性。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6764
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200328015004323李彦_null.pdf(750KB)----限制开放-- 联系获取全文

Recommended Citation:
李彦. 形式化分析方法在OnceAS设计和实现中的应用[D]. 软件研究所. 中国科学院软件研究所. 2006-06-15.
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