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

Compression and verification of embedded software based on timed automata

作　　者：任龙涛[1] 张超 崔磊 魏理豪 周宽久[1,4] 

机构地区：[1]大连理工大学软件学院,辽宁大连116620 [2]广东电网有限责任公司信息中心,广东广州510600 [3]广东电网有限责任公司信息化评测实验室,广东广州510600 [4]中国航天软件评测中心,北京100800

出　　处：《计算机工程与设计》2016年第5期1217-1223,共7页Computer Engineering and Design

摘　　要：利用时间自动机对嵌入式系统进行建模是一种有效方式,但由于时间自动机引入时间维度,导致状态空间是无限的,增加了系统分析验证的难度,为此提出一种时间自动机压缩方法,即条件符号化状态压缩法,对自动机模型进行压缩;在此基础上提出一种时间自动机形式化表示方法,采用有界模型检测的思想形式化表示线性时态逻辑(linear temporal logic,LTL)性质,将需要验证的性质输入可满足性模理论(satisfiability modulo theories,SMT)求解器进行验证,在一定程度上解决了时间自动机"状态爆炸"的问题。To model embedded systems with timed automata is a kind of effective approach due to high real-time and strong concurrency properties,and introducing the time dimension into an automaton brings about infinite state spaces in an automaton,which makes it more difficult to test embedded software systems.A compression algorithm of time automata,namely states compression method of constraint symbolization,was proposed.Consequentially,based on this method,a formalization of timed automata was presented.The linear temporal logic（LTL）properties represented as bounded model checking（BMC）problem can be determined by satisfiability modulo theories（SMT）solving.Through these methods the problem of state explosion of time automata can be solved to some extent.

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术]