基于模型检验的软件可信分析模型

摘要：

随着软件在关键领域的应用日趋普遍,由于软件复杂性导致的各种问题层出不穷,为保证软件的可信性,探索软件可信的自动化分析与验证方法,文中基于模型检验方法提出了一种软件可信分析模型.该模型使用有限状态机(FSA)描述软件的非可信行为属性,使用下推自动机(PDA)描述软件运行中的行为和已知非可信行为,构建已知非可信行为库DPDA.基于模型检验方法自动验证软件是否存在可疑行为,并检查可疑行为是否为非可信行为库中的已知非可信行为.本模型能快速地对软件进行自动化可信分析,有效缓解一般模型检验过程中的状态爆炸问题,为软件可信的自动化验证与评估提供依据.

关键词：模型检验、软件可信分析、有限状态机、可信软件

分类号：TP316(计算技术、计算机技术)

在线出版日期：2012-11-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：35-38