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

• 作者: 安杰 张苗苗
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 时段演算 扩展线性时段不变式 量词线性算术 量词消去
• 年，卷（期）: 2019,（7）
• 所属期刊栏目: 软件形式化验证专题
• 页码范围: 1953-1965
• 页数: 13页
• 分类号: TP311
• 字数: 12024字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005752

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张苗苗	同济大学软件学院	6	6	2.0	2.0
2	安杰	同济大学软件学院	5	2	1.0	1.0