摘要
随着软件在关键领域的应用日趋普遍,由于软件复杂性导致的各种问题层出不穷,为保证软件的可信性,探索软件可信的自动化分析与验证方法,文中基于模型检验方法提出了一种软件可信分析模型。该模型使用有限状态机(FSA)描述软件的非可信行为属性,使用下推自动机(PDA)描述软件运行中的行为和已知非可信行为,构建已知非可信行为库DPDA。基于模型检验方法自动验证软件是否存在可疑行为,并检查可疑行为是否为非可信行为库中的已知非可信行为。本模型能快速地对软件进行自动化可信分析,有效缓解一般模型检验过程中的状态爆炸问题,为软件可信的自动化验证与评估提供依据。
With popular application of software in the key area, the various problems caused by software complexity are emerging all the time. In order to ensure the software trusty and explore automatic analysis and verification method of software trusty ,established a kind of trusted software analysis model according to model checking. First, based on automata theory, untrusted sofiware attributes are described with FSA, unchecked ,software behaviors are described with PDA, untrusted software behaviors that already known are also described by PDA and kept as untrusted software behavior PDA library DPDA. Then the model will check whether unchecked software behaviors have untrusted software attributes using model checking, search DPDA for same untrusted behaviors. This model can analyse untrusted software behaviors, relieve the situation exposure, it is also suitable for automated trust software checking and evaluation.
出处
《计算机技术与发展》
2012年第10期35-38,共4页
Computer Technology and Development
基金
国家"973"重点基础研究发展计划(2007CB311100)
关键词
模型检验
软件可信分析
有限状态机
可信软件
model checking
trusted software analysis
finite state machine
trusted software
