微信服务号

微信订阅号

2025年3月24日 10:51 星期一
首页 > 过刊浏览>2019年第30卷第7期 >1953-1965. DOI:10.13328/j.cnki.jos.005752
PDF HTML阅读 XML下载 导出引用 引用提醒
基于实时自动机的连续时段演算的验证
作者:
作者简介:

安杰(1990-),男,湖北京山人,博士,主要研究领域为形式化方法,混成系统,模型检测;张苗苗(1971-),女,博士,研究员,博士生导师,CCF专业会员,主要研究领域为形式化方法.

通讯作者:

张苗苗,E-mail:miaomiao@tongji.edu.cn

中图分类号:

TP311

基金项目:

国家自然科学基金（61472279）


Verifying Continuous-time Duration Calculus against Real-time Automaton
Author:
Fund Project:

National Natural Science Foundation of China (61472279)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [24]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑.扩展线性时段不变式是时段演算的重要子集.针对实时自动机，提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法.该方法将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题，从而可以采用量词消去技术进行求解.首先，运用符号化的思想，在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段；然后，将每条符号化路径片段转化为一个量词线性算术公式；最后，利用量词消去工具求解.与已有工作相比，基于实时自动机设计了验证算法.另外，降低了验证复杂度，并且加速了验证过程的实际速度.

    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.

    参考文献
    [1] Zhou CC, Hoare CAR, Ravn AP. A calculus of durations. Information Processing Letters, 1991,40(5):269-276.
    [2] Li XS, Zhou CC. Duration calculi:An overview. Chinese Journal of Computers, 1994,(11):842-851(in Chinese with English abstract).
    [3] Halpern JY, Manna Z, Moszkowski BC. A hardware semantics based on temporal intervals. In:Proc. of the 10th Int'l Colloquium on Automata, Languages, and Programming (ICALP). Berlin:Springer-Verlag, 1983. 278-291.[doi:10.1007/BFb0036915]
    [4] Meyer R, Faber J, Hoenicke J, Rybalchenko A. Model checking duration calculus:A practical approach. Formal Aspects of Computing, 2008,20(4):481-505.[doi:10.1007/s00165-008-0082-7]
    [5] Zhou CC, Hansen MR. Duration Calculus:A Formal Approach to Real-Time Systems. Berlin, Heidelberg:Springer-Verlag, 2004.[doi:10.1007/978-3-662-06784-0]
    [6] Zhou CC, Hansen MR, Sestoft P. Decidability and undecidability results for duration calculus. In:Proc. of the 10th Annual Symp. on Theoretical Aspects of Computer Science (STACS). Berlin, Heidelberg:Springer-Verlag, 1993. 58-68.[doi:10.1007/3-540-56503-5_8]
    [7] Zhou CC, Zhang J, Yang L, Li XS. Linear duration invariants. In:Proc. of the 3rd Int'l Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). Berlin, Heidelberg:Springer-Verlag, 1994. 86-109.[doi:10.1007/3-540-58468-4_161]
    [8] Braberman VA, Huang DV. On checking timed automata for linear duration invariants. In:Proc. of the 19th IEEE Real-Time Systems Symp. (RTSS). Washington:IEEE Computer Society, 1998. 264-273.[doi:10.1109/REAL.1998.739752]
    [9] Li XD, Huang DV. Checking linear duration invariants by linear programming. In:Proc. of the Concurrency and Parallelism, Programming, Networking, and Security:The 2nd Asian Computing Science Conf. (ASIAN). Berlin, Heidelberg:Springer-Verlag, 1996. 321-332.[doi:10.1007/BFb0027804]
    [10] Li XD, Huang DV, Zheng T. Checking hybrid automata for linear duration invariants. In:Proc. of the Advances in Computing Science:The 3rd Asian Computing Science Conf. (ASIAN). Berlin, Heidelberg:Springer-Verlag, 1997. 166-180.[doi:10.1007/3-540-63875-X_51]
    [11] Thai P, Huang DV. Verifying linear duration constraints of timed automata. In:Proc. of the 1st Int'l Colloquium on Theoretical Aspects of Computing (ICTAC). Berlin, Heidelberg:Springer-Verlag, 2004. 295-309.[doi:10.1007/978-3-540-31862-0_22]
    [12] Zhang MM, Huang DV, Liu ZM. Verification of linear duration invariants by model checking CTL properties. In:Proc. of the 5th Int'l Colloquium on Theoretical Aspects of Computing (ICTAC). Berlin, Heidelberg:Springer-Verlag, 2008. 395-409.[doi:10. 1007/978-3-540-85762-4_27]
    [13] Zhang MM, Liu ZM, Zhan NJ. Model checking linear duration invariants of networks of automata. In:Proc. of the 3rd Int'l IPM Conf. on Fundamentals of Software Engineering (FSEN). Berlin, Heidelberg:Springer-Verlag, 2009. 244-259.[doi:10.1007/978-3-642-11623-0_14]
    [14] Fränzle M, Hansen MR. Efficient model checking for duration calculus based on branching-time approximations. In:Proc. of the 6th IEEE Int'l Conf. on Software Engineering and Formal Methods (SEFM). Washington:IEEE Computer Society, 2008. 63-72.[doi:10.1109/SEFM.2008.26]
    [15] Fränzle M, Hansen MR. Efficient model checking for duration calculus. Int'l Journal of Software and Informatics, 2009,3(2-3):171-196.
    [16] Zu Q, Zhang MM, Zhu JQ, Zhan NJ. Bounded model-checking of discrete duration calculus. In:Proc. of the 16th Int'l Conf. on Hybrid Systems:Computation and Control (HSCC). New York:ACM, 2013. 213-222.[doi:10.1145/2461328.2461362]
    [17] An J, Zhan NJ, Li XS, Zhang MM, Wang Y. Model checking bounded continuous-time extended linear duration invariants. In:Proc. of the 21st Int'l Conf. on Hybrid Systems:Computation and Control (HSCC). New York:ACM, 2018. 81-90.[doi:10.1145/3178126.3178147]
    [18] Dima C. Real-time automata. Journal of Automata, Languages and Combinatorics, 2001,6(1):3-24.[doi:10.25596/jalc-2001-003]
    [19] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235.
    [20] Tarski A. A Decision Method for Elementary Algebra and Geometry. Berkeley:University of California Press, 1951.
    [21] Collins G. Hauptvortrag:Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In:Proc. of the 2nd GI Conf. on Automata Theory and Formal Languages. Berlin, Heidelberg:Springer-Verlag, 1975. 134-183.[doi:10.1007/3-540-07407-4_17]
    [22] Brown CW. QEPCAD B:A program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin, 2003,37(4):97-108.[doi:10.1145/968708.968710]
    附中文参考文献:
    [2] 李晓山,周巢尘.时段演算综述.计算机学报,1994,(11):842-851.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:2979
  • 下载次数: 5075
  • HTML阅读次数: 2801
  • 引用次数: 0
历史
  • 收稿日期:2018-07-15
  • 最后修改日期:2018-09-28
  • 在线发布日期: 2019-04-03
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19727565位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号