软件学报

作者：安杰,张苗苗

单位：安杰，同济大学 软件学院, 上海 20180411,张苗苗，同济大学 软件学院, 上海 20180402

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

基金：国家自然科学基金（61472279）

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

来源：2019年第7期

《软件学报》期刊编辑部

查看软件学报杂志2019年第7期