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

留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

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

李绍荣, 杨世翰, 吴尽昭

文章导航 > 电子科技大学学报 > 2009 > 38(5): 669-677

李绍荣, 杨世翰, 吴尽昭. Moore机表示的系统迭代设计动态CTL模型检验的不变性研究[J]. 电子科技大学学报, 2009, 38(5): 669-677. doi: 10.3969/j.issn.1001-0548.2009.05.026

引用本文:

李绍荣, 杨世翰, 吴尽昭. Moore机表示的系统迭代设计动态CTL模型检验的不变性研究[J]. 电子科技大学学报, 2009, 38(5): 669-677. doi: 10.3969/j.issn.1001-0548.2009.05.026

LI Shao-rong, YANG Shi-han, WU Jin-zhao. On Invariance of Dynamic CTL Model Checking in Iterative Design of Moore Machine-based System[J]. Journal of University of Electronic Science and Technology of China, 2009, 38(5): 669-677. doi: 10.3969/j.issn.1001-0548.2009.05.026

Citation:

LI Shao-rong, YANG Shi-han, WU Jin-zhao. On Invariance of Dynamic CTL Model Checking in Iterative Design of Moore Machine-based System[J]. Journal of University of Electronic Science and Technology of China, 2009, 38(5): 669-677. doi: 10.3969/j.issn.1001-0548.2009.05.026

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

doi: 10.3969/j.issn.1001-0548.2009.05.026

1.
电子科技大学光电信息学院成都 610054;
2.
中国科学院成都计算机应用研究所成都 610041

基金项目:

国家863计划(2007AA01Z143)

作者简介:
李绍荣(1964-)，男，教授，主要从事复杂系统验证与评估技术方面的研究

中图分类号: TP301.6

On Invariance of Dynamic CTL Model Checking in Iterative Design of Moore Machine-based System

1.
School of Optoelectronic Information,University of Electronic Science and Technology of China Chengdu 610054;
2.
Chengdu Institute of Computer Applications,Chinese Academy of Sciences Chengdu 610041

摘要: 模型检验是系统级设计中验证可信计算系统安全性性质的有效方法。动态模型检验是模型随设计过程而变化的模型检验,动态模型检验过程中遇到的最严重问题之一是模型变化所带来的重复检验代价太高。因此,寻找不变性以避免重复检验显得尤为重要。不变性是一种贯穿系列模型检验而保值为真的性质。该文构建动态模型检验的形式化框架,进而提出基于Moore机描述的流控制系统迭代设计过程的不变性理论,该系统是一种嵌入式控制系统,在可信通信中用以处理数据转换,最后展示了若干非平凡CTL性质在迭代过程中的可保持性。
- 计算树逻辑 /
- 动态模型检验 /
- 不变性 /
- 迭代设计 /
- Moore机
Abstract: Model checking is a promising approach to verifying safety properties of trusted computing systems in the design phase of system-level. Dynamic model checking is the model checking in which the model changes frequently along the design process. A serious problem for dynamic model checking is that the cost of re-checking is too expensive due to model being changed trivially, so a key issue of the problem is to seek invariance in order to avoid the checking repeatedly. An invariance is a true predicate that will remain true throughout a sequence of model checking. In this paper, a formal framework of dynamic model checking is constructed, and an invariance theory is proposed based on an iterative design process of flow control oriented systems described by Moore machines. It is proved that some non-trivial computation tree logic (CTL) properties can be preserved in the iteration.
- computation tree logic /
- dynamic model checking /
- invariance /
- iterative design /
- Moore machine

[1]	李妍, 胡剑浩, 卢浩. 基于部分簇能量互补逻辑的MRF电路设计 . 电子科技大学学报, 2017, 46(5): 648-653. doi: 10.3969/j.issn.1001-0548.2017.05.002
[2]	柳兴, 袁超伟, 杨震, 彭恩达. 移动云计算中一种虚拟机定价与分配方案 . 电子科技大学学报, 2016, 45(2): 197-201.
[3]	陈晓, 江建慧. 动态可配置的两阶段虚拟机容错分配方法 . 电子科技大学学报, 2016, 45(3): 442-447. doi: 10.3969/j.issn.1001-0548.2016.02.022
[4]	王丹琛, 张仕斌, 徐扬, 许宁. 基于业务用户行为的计算机动态取证评估模型研究 . 电子科技大学学报, 2015, 44(6): 921-927. doi: 10.3969/j.issn.1001-0548.2015.06.022
[5]	朱维军, 乔芃喆, 周清雷, 张海宾. 基于时间区间时序逻辑的实时系统统一模型检测 . 电子科技大学学报, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014
[6]	张雪芹, 顾春华, 吴吉义. 异常检测中支持向量机最优模型选择方法 . 电子科技大学学报, 2011, 40(4): 559-563. doi: 10.3969/j.issn.1001-0548.2011.04.017
[7]	叶华, 武继刚. 软硬件协同设计复杂问题的计算模型和算法 . 电子科技大学学报, 2011, 40(3): 333-345. doi: 10.3969/j.issn.1001-0548.2011.03.002
[8]	胡东伟, 陈杰, 石寅, 潘申富, 汪春霆. BPSK调制高动态遥测接收机的设计 . 电子科技大学学报, 2011, 40(5): 691-696. doi: 10.3969/j.issn.1001-0548.2011.05.011
[9]	张贤勇, 熊方, 莫智文, 程伟. 程度与精度的逻辑差粗糙集模型 . 电子科技大学学报, 2010, 39(5): 783-787. doi: 10.3969/j.issn.1001-0548.2010.05.028
[10]	李鑫, 李凡, 刘启和. ER模型的逻辑表示途径 . 电子科技大学学报, 2010, 39(3): 435-439. doi: 10.3969/j.issn.1001-0548.2010.03.024
[11]	向国齐, 严志坚, 黄大贵. 支持向量机替代模型的遗传优化设计 . 电子科技大学学报, 2009, 38(3): 459-462. doi: 10.3969/j.issn.1001-0548.2009.03.034
[12]	王洪, 吕幼新, 汪学刚, 刘磊. 宽带数字接收机的高效FPGA设计 . 电子科技大学学报, 2008, 37(3): 364-365,369.
[13]	王红军, 钟子发. 一种新型的GSM接收机的设计与实现 . 电子科技大学学报, 2006, 35(3): 309-312.
[14]	郭明安, 李斌康, 郝文析, 阮林波, 冯兵. 新型PA高帧频摄像机的设计与实现 . 电子科技大学学报, 2005, 34(1): 77-80.
[15]	余学德, 邱琪, 王学民. 1.25 Gb/s光突发模式接收机的设计 . 电子科技大学学报, 2004, 33(6): 706-709.
[16]	曹刚, 游志胜, 赵树龙. 基于小波隐性马尔可夫树模型的车牌定位 . 电子科技大学学报, 2004, 33(5): 515-518.
[17]	陈隽永, 徐继麟. 超宽带雷达接收机的设计 . 电子科技大学学报, 2000, 29(5): 461-464.
[18]	李贤, 曾广荣, 徐铭. 空间光通信收发端机性能分析与设计 . 电子科技大学学报, 1998, 27(5): 502-505.
[19]	郭旭平, 李在铭. 高速CCD视频摄像机的设计与研究 . 电子科技大学学报, 1998, 27(3): 269-273.
[20]	徐文芳. 化简逻辑函数软件设计 . 电子科技大学学报, 1997, 26(5): 539-543.

WeChat

点击查看大图

计量

文章访问数: 4118
HTML全文浏览量: 128
PDF下载量: 48
被引次数: 0

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

doi: 10.3969/j.issn.1001-0548.2009.05.026

1. 电子科技大学光电信息学院成都 610054;

2. 中国科学院成都计算机应用研究所成都 610041

基金项目:

国家863计划(2007AA01Z143)

作者简介:
李绍荣(1964-)，男，教授，主要从事复杂系统验证与评估技术方面的研究

收稿日期: 2009-08-05
刊出日期: 2009-10-15

中图分类号: TP301.6

关键词:

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

English Abstract

李绍荣, 杨世翰, 吴尽昭. Moore机表示的系统迭代设计动态CTL模型检验的不变性研究[J]. 电子科技大学学报, 2009, 38(5): 669-677. doi: 10.3969/j.issn.1001-0548.2009.05.026

引用本文:

李绍荣, 杨世翰, 吴尽昭. Moore机表示的系统迭代设计动态CTL模型检验的不变性研究[J]. 电子科技大学学报, 2009, 38(5): 669-677. doi: 10.3969/j.issn.1001-0548.2009.05.026

LI Shao-rong, YANG Shi-han, WU Jin-zhao. On Invariance of Dynamic CTL Model Checking in Iterative Design of Moore Machine-based System[J]. Journal of University of Electronic Science and Technology of China, 2009, 38(5): 669-677. doi: 10.3969/j.issn.1001-0548.2009.05.026

Citation:

LI Shao-rong, YANG Shi-han, WU Jin-zhao. On Invariance of Dynamic CTL Model Checking in Iterative Design of Moore Machine-based System[J]. Journal of University of Electronic Science and Technology of China, 2009, 38(5): 669-677. doi: 10.3969/j.issn.1001-0548.2009.05.026

全文HTML

/

下载: 全尺寸图片幻灯片

分享

用微信扫码二维码

分享至好友和朋友圈

返回

期刊在线

编辑办公

友情链接

电子科技大学

版权所有 © 《电子科技大学学报》编辑部

地址: 成都市建设北路二段四号电子科技大学主楼中350室电话: 028-83202308,83207559 Email: xuebao@uestc.edu.cn

本系统由北京仁和汇智信息技术有限公司开发