基于时间自动机的嵌入式软件压缩与验证

作者：任龙涛; 张超; 崔磊; 魏理豪; 周宽久

来源：计算机工程与设计, 2016, 37(05): 1217-1223.

DOI：10.16208/j.issn1000-7024.2016.05.020

• 时间自动机
• 模型验证
• 嵌入式软件
• 状态空间压缩
• 可满足性模理论

利用时间自动机对嵌入式系统进行建模是一种有效方式,但由于时间自动机引入时间维度,导致状态空间是无限的,增加了系统分析验证的难度,为此提出一种时间自动机压缩方法,即条件符号化状态压缩法,对自动机模型进行压缩;在此基础上提出一种时间自动机形式化表示方法,采用有界模型检测的思想形式化表示线性时态逻辑(linear temporal logic,LTL)性质,将需要验证的性质输入可满足性模理论(satisfiability modulo theories,SMT)求解器进行验证,在一定程度上解决了时间自动机"状态爆炸"的问题。

• 单位
  中国航天软件评测中心; 大连理工大学; 广东电网有限责任公司; 广东电网有限责任公司信息中心