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

摘要

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