PVS中cCSP同步语义的形式化
Formalizing cCSP Synchronous Semantics in PVS
摘要：
补偿CSP（Compensating CSP，cCSP）是一种定义为在标准CSP进程代数框架内对长时间运行的业务事务进行建模的语言。在早期的工作中，我们已经定义了语言的跟踪和操作语义。我们通过定义两个语义模型之间的关系，证明了它们之间的一致性。同步在早期的语义定义中是缺失的，而同步是任何进程代数的重要特性。在本文中，我们通过扩展语法和语义来支持同步并定义语义模型之间的关系来解决这个问题。此外，我们通过使用定理证明器PVS机械地验证语义关系来提高我们的证明技术的可扩展性。我们展示了如何将进程代数术语和语义嵌入到PVS中，并使用这些嵌入来证明语义关系。
英文摘要：
Compensating CSP (cCSP) is a language defined to model long running business transactions within the framework of standard CSP process algebra. In earlier work, we have defined both traces and operational semantics of the language. We have shown the consistency between the two semantic models by defining a relationship between them. Synchronization was missing from the earlier semantic definitions which is an important feature for any process algebra. In this paper, we address this issue by extending the syntax and semantics to support synchronization and define a relationship between the semantic models. Moreover, we improve the scalability of our proof technique by mechanically verifying the semantic relationship using theorem prover PVS. We show how to embed process algebra terms and semantics into PVS and to use these embeddings to prove the semantic relationship.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
