Moore机表示的系统迭代设计动态CTL模型检验的不变性研究

• 作者: 吴尽昭 李绍荣 杨世翰
• 来源期刊: 电子科技大学学报
• 学科: 工学
• 关键词: 计算树逻辑 动态模型检验 不变性 迭代设计 Moore机
• 年，卷（期）: 2009,（5）
• 页码范围: 669-677
• 页数: 9页
• 分类号: TP301.6
• 字数: 3098字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-0548.2009.05.026

摘要

模型检验是系统级设计中验证可信计算系统安全性性质的有效方法.动态模型检验是模型随设计过程而变化的模型检验,动态模型检验过程中遇到的最严重问题之一是模型变化所带来的重复检验代价太高.因此,寻找不变性以避免重复检验显得尤为重要.不变性是一种贯穿系列模型检验而保值为真的性质.该文构建动态模型检验的形式化框架,进而提出基于Moore机描述的流控制系统迭代设计过程的不变性理论,该系统是一种嵌入式控制系统,在可信通信中用以处理数据转换,最后展示了若干非平凡CTL性质在迭代过程中的可保持性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李绍荣	电子科技大学光电信息学院	34	234	7.0	14.0
2	吴尽昭	电子科技大学光电信息学院	7	39	2.0	6.0
3	杨世翰	中国科学院成都计算机应用研究所	1	0	0.0	0.0