[1]韩葆 蔡勉.基于模型检验的软件可信分析模型[J].计算机技术与发展,2012,(10):35-38.
　HAN Bao,CAI Mian.Trusted Software Analysis Model Based on Model Checking[J].,2012,(10):35-38.
点击复制

基于模型检验的软件可信分析模型()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
期数:
2012年10期
页码:
35-38
栏目:
智能、算法、系统工程
出版日期:
1900-01-01

文章信息/Info

Title:
Trusted Software Analysis Model Based on Model Checking
文章编号:
1673-629X（2012）10-0035-04
作者:
韩葆 蔡勉
北京工业大学计算机学院
Author(s):
HAN Bao;  CAI Mian
Dept. of Computer, Beijing University of Technology
关键词:
模型检验; 软件可信分析; 有限状态机; 可信软件
Keywords:
model checking;  trusted software analysis;  finite state machine;  trusted software
分类号:
TP316
文献标志码:
A
摘要:
随着软件在关键领域的应用日趋普遍，由于软件复杂性导致的各种问题层出不穷，为保证软件的可信性，探索软件可信的自动化分析与验证方法，文中基于模型检验方法提出了一种软件可信分析模型。该模型使用有限状态机（FSA）描述软件的非可信行为属性，使用下推自动机（PDA）描述软件运行中的行为和已知非可信行为，构建已知非可信行为库DPDA。基于模型检验方法自动验证软件是否存在可疑行为，并检查可疑行为是否为非可信行为库中的已知非可信行为。本模型能快速地对软件进行自动化可信分析，有效缓解一般模型检验过程中的状态爆炸问题，为软件可信的自动化验证与评估提供依据
Abstract:
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

相似文献/References:

[1]邓永杰,陈颖.构件组合的集成测试[J].计算机技术与发展,2013,(07):31.
　DENG Yong-jie,CHEN Ying.Component Composition Based Integration Test[J].,2013,(10):31.
[2]黄吴丹,严俊琦.路由协议的自动形式化验证方法研究[J].计算机技术与发展,2017,27(12):1.
　HUANG Wu-dan,YAN Jun-qi.Research on Automated Formal Verification of Routing Protocols[J].,2017,27(10):1.
[3]王 冠,郝晓星.一种面向 UEFI 模块的形式化建模与验证方法[J].计算机技术与发展,2021,31(12):116.[doi:10. 3969 / j. issn. 1673-629X. 2021. 12. 020]
　WANG Guan,HAO Xiao-xing.A Formal Modeling and Validation Method for UEFI Module[J].,2021,31(10):116.[doi:10. 3969 / j. issn. 1673-629X. 2021. 12. 020]

备注/Memo

备注/Memo:
国家“973”重点基础研究发展计划（2007CB311100）韩葆（1987-），男，硕士研究生，主要研究方向为信息安全；蔡勉，教授，博士，主要研究方向为信息安全、可信计算
更新日期/Last Update: 1900-01-01