带时间约束的LTL公式的模型检测技术及工具实现

实时系统是能够在指定或确定的时间内完成事件处理的计算机应用系统，它的正确性不仅依赖于系统计算的逻辑结果，还依赖于产生这个结果的时间。实时系统在国防以及工业控制等领域的到广泛应用，为保证系统的正确性和可靠性，使用模型检测方法对其进行检测十分重要。 时间自动机是对实时系统进行建模的一种形式化方法，线性时序逻辑（LTL）是当前常用的描述性质的时序逻辑。CTAV是国际上目前唯一的可对时间自动机直接进行线性时序逻辑性质验证的符号化模型检测工具，但CTAV还不能直接检测带时间约束的线性时序逻辑性质，如果要检测带时间约束的线性时序逻辑性质，需要使用者通过手动构造test时间自动机来实现，这增加了使用者的困难。 为了验证时间自动机M是否满足一个带时间约束的线性时序逻辑q， 本文首先在LTL公式转化Büchi自动机的基础上给出了将带时间约束的LTL公式q转化为时间Büchi自动机Bq的方法，其次针对由性质转化而来的时间Büchi自动机Bq（性质自动机）的特点，本文给出了一个构造乘积自动机M*Bq的过程，使得可将验证M是否满足的问题化归为乘积自动机M*Bq的空性检测问题，由于乘积自动机M*Bq是一个时间Büchi自动机，这样通过调用CTAV中以前已实现的关于时间Büchi自动机的空性检测过程就得到了带时间约束的线性时序逻辑关于时间自动机的一个模型检测过程。此外还修改了LU的计算过程，最后给出了实验数据对比，得到了一个比较好的实现方法。 本文还完善了CTAV对UPPAL模型描述语言中函数成分的支持，以及模型检测完成后反例的输出，方便用户对模型的修改和完善。