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

摘要：

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

关键词：安全性、有限自动机、模型检验

所属期刊栏目：39

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60172063

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：48-49,107