作者：李彦; 张文博; 陈宁江j2ee规范模型检查spin
摘要：J2EE规范描述了当前开发应用服务器和分布式多层应用所遵循的技术蓝本。然而，它所使用的自然或半自然语言描述方式并不严格，易产生二义性，套影响J2EE应用服务器实现的正确性和应用服务器之间的兼容性。针对这一问题，本文以EJB2．1规范中的Timer Service为例，研究了一种基于模型检查技术设计与实现规范方法。首先根据规范的描述提出Timer Service的形式化模型，定义了Timer Service的行为；然后使用模型检查工具SPIN对模型进行分析与验证，不仅证明了模型符合规范要求，而且发现并修正了规范中不严格的描述带来的缺陷。以该模型为基础导出了Timer Service的一种设计方案，这种设计已经在中科院软件所研制的OnceAS应用服务器中得到实现，并在J2EE1．4兼容性测试中证明了其正确性。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
