基于定理证明的多核并行程序验证

To specify and verify multi-core parallel programs, a Cylinder Computation Model(CCM) is proposed based on Propositional Projection Temporal Logic(PPTL), the extended PPTL called CCM-PPTL is established including its syntax,semantics and logic laws. Further,the Normal Form (NF) and Normal Form Graph (NFG) are formalized, and satisfiability of CCM-PPTL formulas is investigated. Moreover, the set of axioms and inference rules of CCM-PPTL is defined; the axiomatic system of CCM-PPTL is formalized; the soundness and completeness of CCM-PPTL are also proved. In addition, to make the verification automatically, a prototype of theorem prover for CCM-PPTL based on PVS will be developed. Based on such a proof system and theorem prover, the methodology for specifying and verifying real multi-core parallel programs will be developed.

扩展命题投影时序逻辑Propositional Projection Temporal Logic(PPTL)，提出适合描述多核并行程序的柱面计算模型Cylinder Computation Model(CCM)，建立扩展的命题投影时序逻辑CCM-PPTL系统。研究它的语法，语义和逻辑规则，研究它的范式，范式图及可判定性。定义CCM-PPTL的公理和推理规则，建立CCM-PPTL的公理系统；证明该公理系统的合理性和完备性。对PPTL定理证明器进行扩展，实现基于PVS的CCM-PPTL证明器原型。建立基于CCM-PPTL公理系统和证明器对多核并行程序进行验证的理论和方法。

多核并行程序设计已成为新的程序设计规范。并行程序往往卷入并发程序的概念如并行进程或线程之间的交互和同步，资源的共享和竞争等等。由于并行和并发程序具有内在的复杂性，程序的错误往往隐藏很深，应用程序测试和分析技术很难被发现。因此，如何保障多核计算环境下并行程序的正确性和可靠性，成为计算机科学领域所面临的新的挑战。. 建模、仿真和验证语言（MSVL）是一个基于共享变量模型的并发时序逻辑程序设计语言。本项目主要研究基于MSVL证明理论的多核并行程序验证方法，研究内容包括：1）扩展命题投影时序逻辑 PPTL，定义柱面计算CCM 的语法和语义；2）在扩展的命题投影时序逻辑 CCM-PPTL中，研究相关柱面计算 CCM 的逻辑规则及定理；3）研究扩展的命题投影时序逻辑 CCM-PPTL 的公理系统；4）开发基于扩展的命题投影时序逻辑 CCM-PPTL 的公理系统的验证器；5）研究多核并行程序的验证实例。. 本项目建立了扩展的命题投影时序逻辑系统 CCM-PPTL，建立了该逻辑系统的模型理论包括语法、语义、 逻辑规则以及相关定理；建立了扩展的命题投影时序逻辑 CCM-PPTL 的公理系统，包括公理集合和推理规则集合，并证明了该公理系统的合理性和完备性；建立了基于扩展的命题投影时序逻辑 CCM-PPTL 的公理系统的多核并行程序的验证理论和方法；并给出了验证示范实例；开发了基于扩展的命题投影时序逻辑 CCM-PPTL 的公理系统的验证器原型。基于本项目提出的柱面计算CCM形式验证理论与方法，可以有效提高多核并行程序的正确性和可靠性。