基于实时自动机的连续时段演算的验证  

Verifying Continuous-time Duration Calculus against Real-time Automaton

作　　者：安杰[1] 张苗苗[1] AN Jie;ZHANG Miao-Miao(School of Software Engineering, Tongji University, Shanghai 201804, China)

机构地区：[1]同济大学软件学院

出　　处：《软件学报》2019年第7期1953-1965,共13页Journal of Software

基　　金：国家自然科学基金(61472279)~~

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

关 键 词：时段演算 扩展线性时段不变式 量词线性算术 量词消去 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]