Portal de Periódicos da CAPES

Behavioural analysis of the enterprise javaBeans™ component architecture

2001; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-45139-0_10

1611-3349

Shin Nakajima, Tetsuo Tamai,

Software Reliability and Analysis Research

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