Behavioural analysis of the enterprise JavaBeans component architecture
Shin Nakajima, Tetsuo Tamai · 2001
Abstract. Rigorous description of protocols (a sequence of events) between components is mandatory for specifications of distributed component frameworks. This paper reports an experience in formalizing and verifying behavioural aspects of the Enterprise JavaBeans TM specification with the SPIN model checker. As a result, some potential flaws are identified in the EJB 1.1 specification document. The case study also demonstrates that the SPIN model checker is an effective tool for behavioural analysis of distributed software architecture. 1