Verifying Continuous-time Duration Calculus against Real-time Automaton
Author:
Affiliation:

Clc Number:

TP311

Fund Project:

National Natural Science Foundation of China (61472279)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    Duration calculus is a kind of interval temporal logic, which is designed for specifying and reasoning the properties about the embedded real-time systems and hybrid systems. Extend linear duration invariants (ELDI) is an important subset of duration calculus. In this study, a bounded model checking algorithm of ELDI formulas against real-time automaton is proposed. The bounded model checking problem of ELDI is reduced into the validity problem of Quantified linear real arithmetic (QLRA) formulas, which can be solved by Quantifier elimination (QE) technique. Firstly, by using deep first search algorithm, the real-time automaton is searched to find all the symbolic paths segments which satisfy the constraints of observation time length. Secondly, the paths segments are transformed into QLRA formulas. Finally, the QLRA formulas are solved by QE tools. Thus, compared with the related works, a verification algorithm of ELDIs is proposed against real-time automaton with lower complexity. In addition, the practical speed of verifying process is accelerated.

    Reference
    Related
    Cited by
Get Citation

安杰,张苗苗.基于实时自动机的连续时段演算的验证.软件学报,2019,30(7):1953-1965

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 15,2018
  • Revised:September 28,2018
  • Adopted:
  • Online: April 03,2019
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063