论文部分内容阅读
实时系统是指不仅系统内部的行为及动作的完成与时间有关，而且对系统外部事件(如输入、中断等)的响应都要满足一定时间约束的系统。由于在国防及工业控制等领域应用广泛，因此这类系统的正确性及可靠性逐渐成为研究的热点。本文主要研究基于时间自动机模型的实时系统模型检测技术。
状态空间爆炸问题是制约模型检测技术实际应用的瓶颈。为了缓解状态空间爆炸问题，本文从状态集合的符号化表示方法及状态空间约简技术两个方面出发进行研究工作。
本文定义了表示状态集的符号化方法DS及SDS，用于符号化表示具有整数时钟值的状态，同时给出状态空间遍历过程中的相关算法，用于有限精度时间自动机的模型检测。
为了增强有限精度时间自动机验证过程中的数据共享程度，缩减状态空间，本文给出DS与BDD结合的方法表示状态空间，并设计了相关算法。实验结果表明这种改进方法有效的减小了状态空间遍历过程中占用的存储空间。
此外，本文还将DS与BDD结合的方法用于闭时间自动机的模型检测，提高了可验证系统的规模，并避免了单纯使用BDD记录所有离散状态时对时钟常量大小比较敏感的不足。对状态空间中状态数量及内存占用量的比较表明采用DS与BDD方法结合后的模型检测工具降低了对时钟常量的敏感程度。
在状态空间缩减方面，本文根据已有的时钟最大上下界抽象方法，给出了其在离散语义下的抽象过程，并用于DS与BDD结合的符号化模型检测过程。