投影时序逻辑的备公理系统与形式验证.pdf

摘要 摘 要 投影时序逻辑(Projection TemporalLogic，PTL)是一阶区间时序逻辑(IntervalTemporal 了完全正则表达式的表达能力，能够方便的描述顺序、选择、循环、并行、信号量等 程序结构，可在同一PTL逻辑框架内完成对待验证系统的建模和性质描述，适用于各类 软硬件系统的验证． 。 为采用定理证明的方法对并发及交互式系统验证。本文在有穷论域的前提下 为PTL建立了一个完备公理系统，提出了PTL的范式(Normal Form Normal Normal Graph，NFG)、标记范式(LabeledForm，LNF)和标记范式图(Labeled Form 和无穷时问PTL的判定问题，并证明了有穷时间和无穷时间PTL公理系统的完备性， 下了坚实的理论基础。 本文的主要贡献如下： (1)为PTL提出了一个同时支持有穷时间和无穷时间的公理系统．该公理系统支持 时序项、函数和谓词，这是目前已知的首次全部支持这些项的时序逻辑公理系统．另外。 基于PTL的公理系统证明了大量验证时常用的定理和派生推导规则． 算法。并证明了有穷时间PTL公理系统的完备性。首先给出了NF的定义、证明了NF的 存在性并给出了NF的计算算法．接着基于NF给出了NFG的定义和构造算法．最后，基 穷时间PTL公理系统的完备性． Free 的PTL(Quantifier LabeledNormal 定算法．接着，引入了一般标记范式(Generalized Form LabeledNormal 记范式图(Generalized 一个包含量词的PTL(Quantified 统的完备性． (4)分析了基于PTL进行形式化验证的关键问题，并结合实例展示了基于PTL的定理 证明方法在并发系统验证中的有效性．首先。通过有穷论域下PTL和完全正则表达式相 互直接表达展示了PTL在系统建模和性质描述方面的强大表达能力．接着，介绍了基于 II 投影时序逻辑的完备公理系统与形式验证 框架时序逻辑程序设计语言MSVL的系统建模方法，并提出了基于扩展Kripke结构的系 统建模方法．最后。作为案例研究，使用PTL公式完成了多核处理器上进程调度器的建模 和性质描述。并基于PTL的公理系统以定理证明方法完成了进程调度的正确性验证． 关键词：投影时序逻辑公理系统完备性证明范式图形式化验证 Abstract III Abstract ail Projectiontemporal extensionofthefirstorderinterval logic(PTL)is temporal anew and bothfiniteand logic(ITL)byintroducingtemporaloperator prj supporting infinite hasan offull andcan time．Further，PTLexpressivepower regular express