论文部分内容阅读
投影时序逻辑(Projection Temporal Logic, PTL)是一阶区间时序逻辑(Interval Temporal Logic, ITL)的扩展,引入了全新的投影操作符prj,并且同时支持有穷和无穷模型,具备了完全正则表达式的表达能力,能够方便的描述顺序、选择、循环、并行、信号量等程序结构,可在同一PTL逻辑框架内完成对待验证系统的建模和性质描述,适用于各类软硬件系统的验证.为采用定理证明的方法对并发及交互式系统验证,本文在有穷论域的前提下为PTL建立了一个完备公理系统,提出了PTL的范式(Normal Form, NF)、范式图(Normal Form Graph, NFG)、标记范式(Labeled Normal Form, LNF)和标记范式图(Labeled Normal Form Graph, LNFG)技术,利用NFG和LNFG可描述PTL公式模型的特性分别解决了有穷和无穷时间PTL的判定问题,并证明了有穷时间和无穷时间PTL公理系统的完备性,同时探讨了PTL的表达能力和基于PTL的系统建模方法,为使用PTL进行形式化验证打下了坚实的理论基础。本文的主要贡献如下：(1)为PTL提出了一个同时支持有穷时间和无穷时间的公理系统.该公理系统支持时序项、函数和谓词,这是目前已知的首次全部支持这些项的时序逻辑公理系统.另外,基于PTL的公理系统证明了大量验证时常用的定理和派生推导规则.(2)提出了PTL的NF和NFG,基于NFG技术给出了有穷论域下有穷时间PTL的判定算法,并证明了有穷时间PTL公理系统的完备性.首先给出了NF的定义、证明了NF的存在性并给出了NF的计算算法.接着基于NF给出了NFG的定义和构造算法.最后,基于NFG能够描述PTL公式有穷模型的性质解决了有穷时间PTL的判定问题,并证明了有穷时间PTL公理系统的完备性.(3)提出了PTL的LNF和LNFG,基于LNFG技术给出了有穷论域下无穷时间PTL的判定算法,并证明了无穷时间PTL公理系统的完备性.首先给出了LNF的定义和LNF的计算算法.其次,基于LNF给出了LNFG的定义和构造算法.然后,基于LNFG可描述不含量词的PTL (Quantifier Free PTL, QFPTL)公式有穷和无穷模型的特点,给出了QFPTL公式的判定算法.接着,引入了一般标记范式(Generalized Labeled Normal Form, GLNF)和一般标记范式图(Generalized Labeled Normal Form Graph, GLNFG),并通过GLNFG的缩简技术将一个包含量词的PTL (Quantified PTL, QPTL)公式等价转换为一个QFPTL公式,从而解决了任意PTL公式的判定问题.最后基于PTL公式的可判定性证明了无穷时间PTL公理系统的完备性.(4)分析了基于PTL进行形式化验证的关键问题,并结合实例展示了基于PTL的定理证明方法在并发系统验证中的有效性.首先,通过有穷论域下PTL和完全正则表达式相互直接表达展示了PTL在系统建模和性质描述方面的强大表达能力.接着,介绍了基于框架时序逻辑程序设计语言MSVL的系统建模方法,并提出了基于扩展Kripke结构的系统建模方法.最后,作为案例研究,使用PTL公式完成了多核处理器上进程调度器的建模和性质描述,并基于PTL的公理系统以定理证明方法完成了进程调度的正确性验证.