模型检验软件体系结构研究与进展  

Research and Development of Model Checking Software Architecture

作　　者：张鹏程[1] 李必信[1] 周宇[1] 

机构地区：[1]东南大学计算机科学与工程学院,南京210096

出　　处：《计算机科学》2007年第4期7-12,共6页Computer Science

基　　金：国家自然科学基金(批准号:60473065);计算机软件新技术国家重点实验室(南京大学)课题资助

摘　　要：软件体系结构经过10多年的发展,在体系结构的基础理论、体系结构风格、体系结构描述语言和体系结构建模等方面的研究取得了一系列可喜的成就。目前,就软件体系结构的分析、评价、测试和验证的研究也在如火如荼地进行中。模型检验是一种基于自动机理论的形式验证方法,采用穷举状态空间的方式来证明系统的模型是否满足要验证的属性。同传统的测试和验证的手段相比,模型检验有其自身的优势。为此,越来越多的研究人员正在将模型检验技术应用到软件体系结构的分析和验证中。本文调查了模型检验技术在软件体系结构中的应用现状,剖析了影响软件体系结构模型检验的因素,给出了软件体系结构模型检验的未来主题。In the past ten years, software architecture has made a great step in the research of foundation theory, SA style, architecture description language （ADL）, SA model etc. Currently, many people are doing the research of analysis, evaluation, testing and verification. As a formal verification technique based on automata theory, model checking verifies system＇s attributes by enumerating all its state spaces. Compared with the traditional testing and verification techniques, it has its own advantages. Therefore, more and more researches are applying model checking to analyze and verify quality attributes of SA. In this paper the states of model checking SA are first investigated, the factors affecting to it are analyzed in the second, and the future research topics are debated in the final.

关 键 词：软件体系结构 模型检验 应有属性 形式验证 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]