Hits:

Indexed by:期刊论文

Date of Publication:2016-05-16

Journal:计算机工程与设计

Included Journals:PKU、ISTIC

Volume:37

Issue:5

Page Number:1217-1223

ISSN No.:1000-7024

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

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