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