基于时间区间时序逻辑的实时系统统一模型检测

留言板

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

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

基于时间区间时序逻辑的实时系统统一模型检测

朱维军, 乔芃喆, 周清雷, 张海宾

文章导航 > 电子科技大学学报 > 2014 > 43(5): 712-716

朱维军, 乔芃喆, 周清雷, 张海宾. 基于时间区间时序逻辑的实时系统统一模型检测[J]. 电子科技大学学报, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014

引用本文:

朱维军, 乔芃喆, 周清雷, 张海宾. 基于时间区间时序逻辑的实时系统统一模型检测[J]. 电子科技大学学报, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014

ZHU Wei-jun, QIAO Peng-zhe, ZHOU Qing-lei, ZHANG Hai-bin. Model Checking Real-Time Systems within Unified Approach of Timed Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014

Citation:

ZHU Wei-jun, QIAO Peng-zhe, ZHOU Qing-lei, ZHANG Hai-bin. Model Checking Real-Time Systems within Unified Approach of Timed Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014

基于时间区间时序逻辑的实时系统统一模型检测

doi: 10.3969/j.issn.1001-0548.2014.05.014

1.
郑州大学信息工程学院郑州 450001;
2.
西安电子科技大学计算机学院西安 710071;
3.
河南牧业经济学院信息工程系郑州 450011

基金项目:

国家自然科学基金(U1204608, U1304606, 61373043); 中国博士后科学基金(2012M511588)

作者简介:
朱维军(1976-),男,博士,副教授,主要从事软件形式化方法、实时系统方面的研究.

中图分类号: TP301

Model Checking Real-Time Systems within Unified Approach of Timed Interval Temporal Logic

1.
School of Information Engineering,Zhengzhou University Zhengzhou 450001;
2.
School of Computer Science and Technology,XIDIAN University Xi'an 710071;
3.
School of Information Engineering,Henan University of Animal Husbandry and Economy Zhengzhou 450011

摘要: 在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质. 为此, 该文使用一个离散时间区间时序逻辑公式建立实时系统模型, 使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质, 在此基础上, 离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题. 该文证明了新方法的有效性以及正确性, 为区间实时逻辑这一类的模型检测问题提供了方法.
- 统一模型检测 /
- 实时系统 /
- 可满足性判定 /
- 时间区间时序逻辑
Abstract: There is no method for model checking real-time systems within the same real-time interval logic. To this end, we restrict a real-time logic, called Timed Interval Temporal Logic (TITL), on discrete time domain. And then, we use a TITL formula to construct an interval model and another TITL formula to describe an interval property. On the basis of this, we formalize a novel approach for model checking within the same logical framework based on TITL. The validity and correctness of the method are proved at last.
- model checking within unified logical framework /
- real-time systems /
- satisfiability checking /
- timed interval temporal logic

[1]	曹永立, 杨茂林, 廖勇. 基于MPCP协议的任务最坏阻塞时间分析 . 电子科技大学学报, 2016, 45(6): 1002-1007. doi: 10.3969/j.issn.1001-0548.2016.06.022
[2]	郭文生, 杨国武, 李晓瑜, 高敏. 基于满足性判定的布尔网络环求解算法 . 电子科技大学学报, 2015, 44(6): 881-886. doi: 10.3969/j.issn.1001-0548.2015.06.015
[3]	朱怡安, 黄姝娟, 段俊花, 陆伟. 新的混合关键任务调度算法的研究 . 电子科技大学学报, 2014, 43(2): 268-271,286. doi: 10.3969/j.issn.1001-0548.2014.02.021
[4]	朱维军, 邓淼磊, 周清雷, 张海宾. 扩展命题区间时序逻辑公式可满足性判定算法 . 电子科技大学学报, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023
[5]	王小兵, 段振华. 面向对象的时序逻辑语言 . 电子科技大学学报, 2009, 38(1): 97-101.
[6]	田申, 胡勇, 廖俊必, 黄丹平. 快速Curvelet变换在实时机器视觉系统中的应用 . 电子科技大学学报, 2009, 38(4): 631-635. doi: 10.3969/j.issn.1001-0548.2009.04.036
[7]	廖勇, 陈旭东, 桑楠, 胡林辉, 熊光泽, 朱清新. 分布式实时系统的自适应资源管理中间件 . 电子科技大学学报, 2008, 37(1): 101-104.
[8]	陈涛涛, 田裕鹏. 一种非刚体目标的实时检测与跟踪算法 . 电子科技大学学报, 2007, 36(1): 82-85.
[9]	陈旭东, 朱清新, 廖勇, 匡平, 熊光泽. 一种非周期软实时系统的缓冲设计方法 . 电子科技大学学报, 2007, 36(3): 548-550.
[10]	张海涛, 艾云峰. 一种分布式实时嵌入式系统的调度分析算法 . 电子科技大学学报, 2007, 36(3): 489-492.
[11]	廖勇, 熊光泽, 陈旭东, 桑楠, 朱清新. 分布式实时嵌入式系统端到端性能确保 . 电子科技大学学报, 2007, 36(3): 541-544.
[12]	吴琦, 熊光泽, 廖勇. DVS系统硬实时周期任务动态调度算法 . 电子科技大学学报, 2007, 36(5): 842-845.
[13]	陈争航, 李辉. 基于可寻址控制器的用户实时管理系统 . 电子科技大学学报, 2005, 34(3): 392-395.
[14]	王亮, 雷航. 基于资源回收的容错单调比率调度 . 电子科技大学学报, 2004, 33(4): 438-441.
[15]	雷航. 基于任务链的实时多任务软件可靠性建模 . 电子科技大学学报, 2004, 33(2): 158-161.
[16]	骆志刚, 谭浩, 刘锦德. 一个实时CORBA的动态调度服务模型 . 电子科技大学学报, 2001, 30(6): 618-624.
[17]	陈文宇, 桑楠. 分布式实时计算系统的一种调试方法 . 电子科技大学学报, 2001, 30(5): 503-506.
[18]	全萍. 一种外接微机实时数据处理集成系统 . 电子科技大学学报, 1997, 26(5): 544-548.
[19]	雷航, 熊光泽, 刘锦德. 实时多任务系统的超时故障分析 . 电子科技大学学报, 1997, 26(3): 273-278.
[20]	雷航, 熊光泽, 刘锦德. 基于任务模块的实时软件可靠性模型 . 电子科技大学学报, 1997, 26(1): 70-74.

WeChat

点击查看大图

计量

文章访问数: 3330
HTML全文浏览量: 88
PDF下载量: 81
被引次数: 0

基于时间区间时序逻辑的实时系统统一模型检测

doi: 10.3969/j.issn.1001-0548.2014.05.014

1. 郑州大学信息工程学院郑州 450001;

2. 西安电子科技大学计算机学院西安 710071;

3. 河南牧业经济学院信息工程系郑州 450011

基金项目:

国家自然科学基金(U1204608, U1304606, 61373043); 中国博士后科学基金(2012M511588)

作者简介:
朱维军(1976-),男,博士,副教授,主要从事软件形式化方法、实时系统方面的研究.

收稿日期: 2013-06-08
修回日期: 2014-07-08
刊出日期: 2014-10-15

中图分类号: TP301

关键词:

摘要: 在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质. 为此, 该文使用一个离散时间区间时序逻辑公式建立实时系统模型, 使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质, 在此基础上, 离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题. 该文证明了新方法的有效性以及正确性, 为区间实时逻辑这一类的模型检测问题提供了方法.

English Abstract

朱维军, 乔芃喆, 周清雷, 张海宾. 基于时间区间时序逻辑的实时系统统一模型检测[J]. 电子科技大学学报, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014

引用本文:

朱维军, 乔芃喆, 周清雷, 张海宾. 基于时间区间时序逻辑的实时系统统一模型检测[J]. 电子科技大学学报, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014

ZHU Wei-jun, QIAO Peng-zhe, ZHOU Qing-lei, ZHANG Hai-bin. Model Checking Real-Time Systems within Unified Approach of Timed Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014

Citation:

ZHU Wei-jun, QIAO Peng-zhe, ZHOU Qing-lei, ZHANG Hai-bin. Model Checking Real-Time Systems within Unified Approach of Timed Interval Temporal Logic[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(5): 712-716. doi: 10.3969/j.issn.1001-0548.2014.05.014

全文HTML

/

下载: 全尺寸图片幻灯片

分享

用微信扫码二维码

分享至好友和朋友圈

返回

期刊在线

编辑办公

友情链接

电子科技大学

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

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

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