Advances in the Component Verification Technology Based on Model Checking

Due to its high automation and completeness, and strong complementarity with component technology, model checking plays an increasingly important role in the analysis and verification of trustworthy properties of component-based systems. Therefore, model checking technology is applied more and more widely to ensure the high trustworthy properties of safety critical applications, and gradually penetrates into the development process of component-based systems. It has obviously blocked the development of model checking based component verification that there is no review work appeared on the topic. As a result, presented in this paper is a review of analysis and discussion on the research progresses of model checking based component verification methods in recent years. In this paper, the model checking based component verification methods are classified into system specification model based and source code based verification methods, and the states of the art of these methods are summarized in detail. The relationship of model checking and component trustworthy properties verification is discussed firstly. Then SOFA, Fractal, CORBA and other component model based verification methods, and static and dynamic source code based verification methods are summarized respectively. The main challenges and future development directions of model checking based component verification technology are pointed out finally.