|
|||||
|
|
| 基于模型检验的软件可信分析模型 | |
| 作者姓名： | 韩葆 蔡勉 |
| 作者单位： | 北京工业大学 计算机学院,北京 100124 |
| 摘 要： | 随着软件在关键领域的应用日趋普遍,由于软件复杂性导致的各种问题层出不穷,为保证软件的可信性,探索软件可信的自动化分析与验证方法,文中基于模型检验方法提出了一种软件可信分析模型.该模型使用有限状态机(FSA)描述软件的非可信行为属性,使用下推自动机(PDA)描述软件运行中的行为和已知非可信行为,构建已知非可信行为库DPDA.基于模型检验方法自动验证软件是否存在可疑行为,并检查可疑行为是否为非可信行为库中的已知非可信行为.本模型能快速地对软件进行自动化可信分析,有效缓解一般模型检验过程中的状态爆炸问题,为软件可信的自动化验证与评估提供依据. |
| 关 键 词： | 模型检验 软件可信分析 有限状态机 可信软件 |
| 本文献已被 万方数据 等数据库收录！ | |