%0 Journal Article
%T A Case Study in Implementing J2EE Specification Based on Model Checking<br>基于模型检查实现J2EE规范的实例研究
%A LI Yan
%A ZHANG Wen-Bo
%A CHEN Ning-Jiang
%A <br>李彦
%A 张文博
%A 陈宁江
%J 计算机科学
%D 2006
%I 
%X 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.
%K SPIN<br>J2EE规范
%K 模型检查
%K SPIN
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=17708F730A7923D1&yid=37904DC365DD7266&vid=27746BCEEE58E9DC&iid=59906B3B2830C2C5&sid=D537C66B6404FE57&eid=01622E3E475F966C&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=12