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

摘要

利用时间自动机对嵌入式系统进行建模是一种有效方式,但由于时间自动机引入时间维度,导致状态空间是无限的,增加了系统分析验证的难度,为此提出一种时间自动机压缩方法,即条件符号化状态压缩法,对自动机模型进行压缩；在此基础上提出一种时间自动机形式化表示方法,采用有界模型检测的思想形式化表示线性时态逻辑(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 con-currency 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 com-pression method of constraint symbolization,was proposed.Consequentially,based on this method,a formalization of timed au-tomata 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.