论文部分内容阅读
实时系统是指能及时响应外部发生的事件，并以足够快的速度完成对事件处理的计算机应用系统。实时系统应用的场合往往要求其正确性和可靠性能够得到保证，但是由于涉及并发、不确定性以及时间约束等因素，实时系统设计的正确性很难把握。为了确保实时系统的正确性和可靠性，发现系统设计中可能存在的缺陷，利用模型检测技术和工具对其进行分析检测是十分重要的。
时间自动机是实时系统常用的一种形式化模型，LTL是一种常用的时序逻辑语言。本文将介绍实时系统的一个基于时间自动机模型的LTL性质检测工具CTAV。本文介绍了CTAV的设计框架，重点介绍了对CTAV中LTL性质检测过程的优化和改进，对比研究了各种优化策略对检测效率和检测能力的影响。这些优化策略包括改进时间自动机复合的计算生成过程、引入BDD利用BDD的数据共享降低检测过程的空间消耗、把一些状态空间削减的优化方案引入非空性模型检测、利用编码压缩技术减少状态存储占用的内存空间。实验结果表明这些优化策略改进了CTAV的检测能力。
本文还介绍了时间自动机基于BDD表示的符号化LTL性质检测的一些研究工作。主要介绍了用BDD表示时间约束、状态迁移等以及通过BDD操作来完成后继状态的生成。