一种系统安全性的形式化验证方法

• 作者: 吕永波 张仲义 王海峰
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 安全性 有限自动机 模型检验
• 年，卷（期）: 2003,（4）
• 所属期刊栏目: 博士论坛
• 页码范围: 48-49,107
• 页数: 3页
• 分类号: TP301
• 字数: 3278字
• 语种: 中文
• DOI: 10.3321/j.issn:1002-8331.2003.04.014

摘要

随着计算机系统应用的深入和广泛,系统安全性越来越成为人们关注的焦点,形式化模型检验是解决系统特性验证问题的一种有效途径,用有限自动机表示系统的设计和实现,用计算树逻辑CTL(Computational Tree Logic)公式表示系统的安全特性,探讨了系统安全性形式化验证的方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王海峰	北方交通大学电子信息工程学院	9	111	6.0	9.0
2	吕永波	北方交通大学系统工程研究所	13	330	7.0	13.0
3	张仲义	北方交通大学自动化系统研究所	33	574	11.0	23.0