Paper Info
Title
Behavioural analysis of the enterprise JavaBeans component architecture
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 Java Beans™ 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.
Year
Venue
Keywords
2001
SPIN
verifying behavioural aspect,spin model checker,specification document,behavioural analysis,rigorous description,component framework,effective tool,potential flaw,case study,enterprise java beans,enterprise javabeans component architecture
Field
DocType
ISBN
Architecture,Programming language,Model checking,Computer science,Behavioural analysis,Distributed software architecture,Enterprise JavaBeans,Component-based software engineering,Java,SPIN model checker
Conference
3-540-42124-6
Citations 
PageRank 
References 
7
0.62
12
Authors
2
Name
Order
Citations
PageRank
Shin Nakajima11507216.49
Tetsuo Tamai233433.27