Java Beans is a standard for software components. For checking the consistency of the Java Beans semantic constraints with its implementation, a formal Java Beans description language (JBDL) and a dynamic model checking method are proposed in this paper. The authors contribute an efficient symbolic model checking approach using T³BDD. The approach is based on three valued semantics for JBDL formulas and a kind of abstract model which is dynamically established and evolved during Bean’s execution.