| 题名: | 基于模型检查实现J2EE规范的实例研究 |
| 其他题名: | a case study in implementing j2ee specification based on model checking
|
| 作者: | 李彦
; 张文博
; 陈宁江
|
| 关键词: | J2EE规范
; 模型检查
; SPIN
; 基于模型
; 检查工具
; 规范要求
; Model Checking
; 应用服务器
; 描述方式
; 设计方案
; 兼容性测试
; 形式化模型
; 分析与验证
; 自然语言
; 证明
; 使用模型
; 技术设计
; 规范描述
; 规范方法
; 多层应用
; 中科院
; 分布式
; 二义性
|
| 刊名: | 计算机科学
|
| 发表日期: | 2006
|
| 卷: | 33, 期:12, 页:249-254 | | 部门归属: | 中国科学院软件研究所软件工程技术中心,北京,100080;中国科学院软件研究所计算机科学重点实验室,北京,100080;中国科学院研究生院,北京,100080;中国科学院软件研究所软件工程技术中心,北京,100080;中国科学院软件研究所计算机科学重点实验室,北京,100080;中国科学院研究生院,北京,100080;中国科学院软件研究所软件工程技术中心,北京,100080;中国科学院软件研究所计算机科学重点实验室,北京,100080;中国科学院研究生院,北京,100080
|
| 摘要: | J2EE规范描述了当前开发应用服务器和分布式多层应用所遵循的技术蓝本.然而,它所使用的自然或半自然语言描述方式并不严格,易产生二义性,会影响J2EE应用服务器实现的正确性和应用服务器之间的兼容性.针对这一问题,本文以EJB2.1规范中的Timer Service为例,研究了一种基于模型检查技术设计与实现规范方法.首先根据规范的描述提出Timer Service的形式化模型,定义了Timer Service的行为;然后使用模型检查工具SPIN对模型进行分析与验证,不仅证明了模型符合规范要求,而且发现并修正了 |
| 语种: | 中文
|
| 内容类型: | 期刊论文
|
| URI标识: | http://ir.iscas.ac.cn/handle/311060/11746
|
| Appears in Collections: | 软件工程技术研究开发中心 _期刊论文
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| 基于模型检查实现J2EE规范的实例研究.pdf（572KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
李彦,张文博,陈宁江. 基于模型检查实现J2EE规范的实例研究[J]. 计算机科学,2006-01-01,33(12):249-254.
|
|
|
