首页 | 本学科首页   官方微博 | 高级检索  
     检索      

基于实时自动机的连续时段演算的验证
引用本文:安杰,张苗苗.基于实时自动机的连续时段演算的验证[J].软件学报,2019,30(7):1953-1965.
作者姓名:安杰  张苗苗
作者单位:同济大学 软件学院, 上海 201804,同济大学 软件学院, 上海 201804
基金项目:国家自然科学基金(61472279)
摘    要:时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑.扩展线性时段不变式是时段演算的重要子集.针对实时自动机,提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法.该方法将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题,从而可以采用量词消去技术进行求解.首先,运用符号化的思想,在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段;然后,将每条符号化路径片段转化为一个量词线性算术公式;最后,利用量词消去工具求解.与已有工作相比,基于实时自动机设计了验证算法.另外,降低了验证复杂度,并且加速了验证过程的实际速度.

关 键 词:时段演算  扩展线性时段不变式  量词线性算术  量词消去
收稿时间:2018/7/15 0:00:00
修稿时间:2018/9/28 0:00:00

Verifying Continuous-time Duration Calculus against Real-time Automaton
AN Jie and ZHANG Miao-Miao.Verifying Continuous-time Duration Calculus against Real-time Automaton[J].Journal of Software,2019,30(7):1953-1965.
Authors:AN Jie and ZHANG Miao-Miao
Institution:School of Software Engineering, Tongji University, Shanghai 201804, China and School of Software Engineering, Tongji University, Shanghai 201804, China
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.
Keywords:duration calculus  extended linear duration invariants  quantified linear real arithmetic  quantifier elimination
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载免费的PDF全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号