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

作者：张鹏程; 李必信; 周宇

来源：计算机科学, 2007, (04): 7-12.

• 软件体系结构
• 模型检验
• 应有属性
• 形式验证 Software architecture
• Model checking
• Desired properties
• Formal verification

软件体系结构经过10多年的发展,在体系结构的基础理论、体系结构风格、体系结构描述语言和体系结构建模等方面的研究取得了一系列可喜的成就。目前,就软件体系结构的分析、评价、测试和验证的研究也在如火如荼地进行中。模型检验是一种基于自动机理论的形式验证方法,采用穷举状态空间的方式来证明系统的模型是否满足要验证的属性。同传统的测试和验证的手段相比,模型检验有其自身的优势。为此,越来越多的研究人员正在将模型检验技术应用到软件体系结构的分析和验证中。本文调查了模型检验技术在软件体系结构中的应用现状,剖析了影响软件体系结构模型检验的因素,给出了软件体系结构模型检验的未来主题。

• 单位
  计算机软件新技术国家重点实验室; 南京大学; 东南大学