-
题名基于模型检验的软件可信分析模型
被引量：1
- 1
-
-
作者
韩葆
蔡勉
-
机构
北京工业大学计算机学院
-
出处
《计算机技术与发展》
2012年第10期35-38,共4页
-
基金
国家"973"重点基础研究发展计划(2007CB311100)
-
文摘
随着软件在关键领域的应用日趋普遍,由于软件复杂性导致的各种问题层出不穷,为保证软件的可信性,探索软件可信的自动化分析与验证方法,文中基于模型检验方法提出了一种软件可信分析模型。该模型使用有限状态机(FSA)描述软件的非可信行为属性,使用下推自动机(PDA)描述软件运行中的行为和已知非可信行为,构建已知非可信行为库DPDA。基于模型检验方法自动验证软件是否存在可疑行为,并检查可疑行为是否为非可信行为库中的已知非可信行为。本模型能快速地对软件进行自动化可信分析,有效缓解一般模型检验过程中的状态爆炸问题,为软件可信的自动化验证与评估提供依据。
-
关键词
模型检验
软件可信分析
有限状态机
可信软件
-
Keywords
model checking
trusted software analysis
finite state machine
trusted software
-
分类号
TP316
[自动化与计算机技术—计算机软件与理论]
-
