Behavioural analysis of component framework with multi-valued transition system

Model-checking is a promising technique for the verification and validation of systems. Practical systems need complicated design descriptions because they often refer to situations concerning exceptional cases in addition to normal, regular behaviour. Since properties deal with many exceptional cases, the property formulae to be verified become complicated and hard to understand. Further, as both system and property descriptions are complicated, the state space searched in the model-checking process becomes large, which affects execution performance. This paper employs a model-checking technique based on multivalued transition systems to reduce such complexities. It discusses advantages by applying the idea to an example case of the behavioural analysis of the EJB component framework.