全部 标题 作者
关键词 摘要

OALib Journal期刊
ISSN: 2333-9721
费用:99美元

查看量下载量

相关文章

更多...

A Case Study in Implementing J2EE Specification Based on Model Checking
基于模型检查实现J2EE规范的实例研究

Keywords: SPIN
J2EE规范
,模型检查,SPIN

Full-Text   Cite this paper   Add to My Lib

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 such as ambiguity, incorrectness and incompatibility. In this paper, a specification design&implementatation approach based on model checking technology is discussed to solve such problems. Semantic models are applied on the Timer Service in EJB TM Specification 2.1 and formally verified. Using the SPIN model checker, defects both in the design of the model and in the expressions of J2EE specification are discovered and corrected. The process resulted in a faultless and highly compatible model, and based on which, a design of Timer Service is exported. This design has implemented in OnceAS and passed the J2EE1.4 CTS test.

Full-Text

Contact Us

service@oalib.com

QQ:3279437679

WhatsApp +8615387084133