基于模型检查实现J2EE规范的实例研究

计算机科学 ›› 2006, Vol. 33 ›› Issue (12): 249-254.

• 计算机网络与信息安全 • 上一篇下一篇

基于模型检查实现J2EE规范的实例研究

出版日期:2018-11-17 发布日期:2018-11-17
基金资助:
973计划：网构软件中间件平台模型和框架研究（2002CB312005）;863计划：网络环境的系统软件核心技术及运行平台（2001AA113010）;863计划：面向新型ERP的可重配Web应用服务器的研究与应用（2003AA413010）.

Online:2018-11-17 Published:2018-11-17

摘要/Abstract

摘要： J2EE规范描述了当前开发应用服务器和分布式多层应用所遵循的技术蓝本。然而，它所使用的自然或半自然语言描述方式并不严格，易产生二义性，套影响J2EE应用服务器实现的正确性和应用服务器之间的兼容性。针对这一问题，本文以EJB2．1规范中的Timer Service为例，研究了一种基于模型检查技术设计与实现规范方法。首先根据规范的描述提出Timer Service的形式化模型，定义了Timer Service的行为；然后使用模型检查工具SPIN对模型进行分析与验证，不仅证明了模型符合规范要求，而且发现并修正了

关键词: J2EE规范模型检查 SPIN

Abstract: J2EE specifications provide the technique blue-prints of the current development of application servers and distributed multi-layer applications. However, the J2EE specifications are expressed in nature/half-nature language, which brings vulnerabilities s

Key words: J2EE specification, Model checking,SPIN

. 基于模型检查实现J2EE规范的实例研究[J]. 计算机科学, 2006, 33(12): 249-254. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

基于模型检查实现J2EE规范的实例研究

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 0

Metrics

本文评价

推荐阅读 0