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

A Case Study in Implementing J2EE Specification Based on Model Checking

J2EE规范描述了当前开发应用服务器和分布式多层应用所遵循的技术蓝本。然而,它所使用的自然或半自然语言描述方式并不严格,易产生二义性,会影响J2EE应用服务器实现的正确性和应用服务器之间的兼容性。针对这一问题,本文以EJB2.1规范中的TimerService为例,研究了一种基于模型检查技术设计与实现规范方法。首先根据规范的描述提出TimerService的形式化模型,定义了TimerService的行为;然后使用模型检查工具SPIN对模型进行分析与验证,不仅证明了模型符合规范要求,而且发现并修正了规范中不严格的描述带来的缺陷。以该模型为基础导出了TimerService的一种设计方案,这种设计已经在中科院软件所研制的OnceAS应用服务器中得到实现,并在J2EE1.4兼容性测试中证明了其正确性。

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 EJBTM 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.