|
计算机科学 2006
A Case Study in Implementing J2EE Specification Based on Model Checking
|
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.