基于 SAT 的扩展时序逻辑的符号化模型检验

随着计算机软硬件设计复杂性的日益增加，系统设计和实现的正确性越来越难以得到保证。模型检验方法被证明为行之有效的系统正确性验证手段。模型检验问题所遇到的瓶颈在于目标状态空间的爆炸，它限制了模型检验工具所能处理问题的规模。符号化模型检验能够有效的缩减模型检验的效率，提高其规模。其中，基于 SAT 的符号化模型检验算法能力尤为突出。. 目前，具有完备 omega-正规性质表达能力的模型检验问题越来越受到广泛关注，它们中的某些已经成为工业界的规约标准。扩展时序逻辑（ETL）是这一类语言的公共原型。本课题拟研究三类扩展时序逻辑基于 SAT 的符号模型检验算法（包括 BMC 算法和 UBMC 算法），并实现其相关工具

模型检验技术是计算机软硬件系统正确性保障的重要手段，该技术的主要应用平静在于“状态空间爆炸问题”。符号化技术被证明是一种行之有效 的降低模型检验时空开销的手段。同时，伴随着 SAT 求解的技术突破,其应用逐步扩展到符号化模型检验领域。此外，正规性质的验证问题由其理论意义和应用价值的重要性，使得其在模型检验领域一度受到广泛关注。本项目的主要关注点在于基于 SAT 的各类线性框架下时序逻辑的符号化模型检验问题。主要工作包括：.1. 以扩展时序逻辑（ETL）为典型用例，给出了基于 SAT 的扩展时序逻 辑的模型检验算法及一般框架。.2. 针对线性时序逻辑符号化模型检验问题，提出了“保持反例的规约化简”技术（CePRe）， 该技术可有效降低符号化模型检验时空开销。.3. 给出了语法与语义相结合的 LTL 限界模型检验编码算法，该算法能够 有效的提高编码效率，并能够方便的计算完备阈值。.4. 对于非限界模型检验,给出了可并行实现的双向 PDR 算法，可提高验证效率。.5. 同时针对“模型等价性检查”、”基于重写的运行时验证” 以及 “概率模型检验算法优化”等问题进行了相关研究。.6. 上述主要算法集成在两个工具 ENuSMV（Ver1.2）以及 Reach 中，并均已开源发布。.5. 同时针对“模型等价性检查”、”基于重写的运行时验证”以及“概率模型 检验算法优化”等问题进行了相关研究。.6. 上述主要算法集成在两个工具ENuSMV(Ver1.2)以及Reach中，并 均已开源发布。