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