论文摘要
模型检测方法是最近二十年来最成功的自动验证技术之一,目前已经广泛应用于有穷状态系统(包括通信协议和电路设计)的分析和验证。实时系统的安全性至关重要,模型检测方法可以有效的帮助发现实时系统设计中的一些缺陷或错误,进而提高系统的安全性。 目前国际上有很多实时系统模型检测理论和方法的研究,也存在一些模型检测算法和验证工具,这些工具的大部分或者是基于离散语义模型,或者是基于连续语义模型。 本文介绍的有限精度时间自动机是时间自动机(连续时间语义)的一种语义简化,其有限精度语义结合了连续语义和离散语义各自的优点,既可以描述异步系统,同时由于时钟取值为非负整数,因而相应的模型检测算法也比较简单。基于有限精度时间自动机理论,我们实现了实时系统模型检测工具FPIAT,用于实时系统的可达性分析和验证。并且工具FPTAT实现了一种符号化方法,在模型检测实验中取得了良好效果。 论文的主要工作如下: 1) 设计了基于有限精度时间自动机理论和符号化模型检测方法的实时系统模型检测算法,实现了实时系统模型检测工具FPZAT,通过实验研究证明了其良好的算法效率。 2) 实现了一种符号化方法,即SDS数据结构符号化表示状态空间的状态集,并提出了基于符号化方法的两级Hash索引结构组织状态空间。 3) 此外,还将活动时钟理论应用到基于有限精度时间自动机理论的模型检测中,有效的减少了状态的存储空间,提高了模型检测效率。