Volume 43 Issue 5
Apr.  2017
Article Contents
Article Navigation >  Journal of University of Electronic Science and Technology of China  > 2014  >  43(5): 712-716

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
shu

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

doi: 10.3969/j.issn.1001-0548.2014.05.014
  • 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

  • Received Date: 2013-06-08
  • Rev Recd Date: 2014-07-08
  • Publish Date: 2014-10-15
  • 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.
  • 加载中
通讯作者: 陈斌, bchen63@163.com
  • 1. 

    沈阳化工大学材料科学与工程学院 沈阳 110142

  1. 本站搜索
  2. 百度学术搜索
  3. 万方数据库搜索
  4. CNKI搜索
Get Citation
PDF
XML

Article Metrics

Article views(3514) PDF downloads(83) Cited by()

Related
Proportional views

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

doi: 10.3969/j.issn.1001-0548.2014.05.014
  • 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
  • Received Date: 2013-06-08
  • Rev Recd Date: 2014-07-08
  • Publish Date: 2014-10-15

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.

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
shu

    HTML

Catalog

    Journal Online

    Author's Notes

    Links

    Copyright © 《电子科技大学学报》编辑部

    Address: Room 350, central building, University of Electronic Science and Technology, No.4, Section 2, Jianshe North Road, Chengdu Tel: 028-83202308,83207559 Email: xuebao@uestc.edu.cn

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

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return