形式化分析方法在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模型检查环境验证了连接池的实现并发现了其中的问题，以最直接的方式提升了系统的可靠性。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 70 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6764]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 李彦. 形式化分析方法在OnceAS设计和实现中的应用[D]. 软件研究所. 中国科学院软件研究所. 2006. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。