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