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

• 作者: 蔡勉 韩葆
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 模型检验 软件可信分析 有限状态机 可信软件
• 年，卷（期）: 2012,（10）
• 页码范围: 35-38
• 分类号: TP316
• 字数: 5373字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	蔡勉	北京工业大学计算机学院	22	150	8.0	11.0
2	韩葆	北京工业大学计算机学院	1	2	1.0	1.0