高级检索

    基于模型检验的构件验证技术研究进展

    Advances in the Component Verification Technology Based on Model Checking

    • 摘要: 模型检验以其自动化程度和完备性高、与构件技术互补性强等特点,在软件构件可信性质的分析和验证中发挥着日益重要的作用.将基于模型检验的构件验证方法分为基于系统规约模型的验证和基于源代码的验证,分别对其研究现状和发展动态进行了详细的综合评述.首先对模型检验与构件可信性质验证的关系进行了探讨,接着对基于SOFA,Fractal,CORBA及各种特定构件模型的验证方法和基于转化思想的源码验证、面向源码的直接验证及面向可执行代码的动态验证方法分别进行了评述.最后,指出了基于模型检验的构件验证技术所面临的主要挑战和未来的发展方向.

       

      Abstract: 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.

       

    /

    返回文章
    返回