框架时序逻辑程序语言MSVL的形式语义

论文摘要

形式语义是对软件系统进行形式化验证和分析的重要理论基础。程序语言的语义可以帮助人们更好的理解、执行、分析软件系统。操作语义有助于语言的实现,公理语义有利于程序的验证,指称语义在强大的数学理论支持下为程序的含义提供了精确的数学描述。时序逻辑程序设计是一种新型的程序设计范式,程序的具体执行和性质的描述可以在同一逻辑框架内表示,适用于并发系统的建模、模拟和验证。尽管研究人员开发了相关的解释器来执行各类时序逻辑程序语言,时序逻辑及其可执行子集被广泛地应用于系统的规范和验证中,但是到目前为止,至少在区间时序逻辑程序语言中,还没有一套系统而完整的形式语义。本文以区间时序逻辑程序语言MSVL为研究对象,分别从模型语义、操作语义、公理语义三条主线来研究区间时序逻辑程序的形式语义,并对三种语义之间的一致性、互补性进行分析和证明。本文研究了MSVL语言的极小模型语义。由于MSVL语言中的框架技术破坏了逻辑的单调性,传统的规范模型已不再适用于捕获该语言的模型语义。因此,我们提出了极小模型理论并证明了极小模型的存在性定理。为了正确理解程序语言的执行过程,本文研究了MSVL语言的结构化操作语义。首先定义了一种新的适用于描述区间时序逻辑程序语言语义的表达式格局和命令格局。其次给出了带有时态操作符的算术表达式和布尔表达式的求值规则,以及程序的状态迁移系统和区间迁移系统。状态迁移系统包括将一个程序化简为与其等价的正则形的语义等价规则和状态上的迁移规则。区间迁移系统给出了将程序从一个状态迁移到下一个状态的区间迁移规则。进一步,我们研究了两类迁移系统的性质,并证明了操作语义和基于模型理论的极小模型语义之间的一致性。最后基于本文提出的操作语义,开发了具有对软硬件系统进行建模、模拟和验证功能的MSVL语言的解释器。为了实现在同一逻辑框架内对并发系统进行建模和验证的目的,本文研究了MSVL语言的公理语义。在该方法中,MSVL语言作为程序设计语言来描述系统行为(系统建模),命题投影时序逻辑作为断言语言描述系统性质。这样,系统的模型和性质的规范可以用同一逻辑记号表示,简化了验证在不同形式化记号之间转换的复杂过程。进一步,我们给出将程序推演为正则形的状态公理和状态推演规则以及程序在区间上的公理和推演规则,这些规则在将程序从一种状态转换到另一种状态的同时实现程序性质的验证。另外,基于MSVL语言的操作语义,我们证明了该公理系统的可靠性和相对完备性。最后,使用该语言的公理语义对一个应用实例的完全正则性质进行了形式化验证。

论文目录

• Abstract（chinese）
• Abstract
• List of Figures
• List of Tables
• Chapter 1 Introduction
• 1.1 Formal Semantics Methodologies
• 1.1.1 Operational Semantics
• 1.1.2 Denotational Semantics
• 1.1.3 Axiomatic Semantics
• 1.2 Temporal Logic and Temporal Logic Programming
• 1.2.1 Temporal Logic
• 1.2.2 Temporal Logic Programming
• 1.2.3 Existing Problems
• 1.3 Contributions
• 1.4 Thesis Organization
• Chapter 2 Projection Temporal Logic
• 2.1 Propositional Projection Temporal Logic
• 2.2 First Order Projection Temporal Logic
• 2.2.1 Syntax and Semantics
• 2.2.2 Satisfaction and Validity
• 2.2.3 Derived Formulas and Logic Laws
• 2.2.4 Replacement of Variables
• 2.3 Conclusion
• Chapter 3 Programming Language MSVL
• 3.1 The History of MSVL
• 3.2 Framing
• 3.3 MSVL Programs
• 3.3.1 Expressions and Statements
• 3.3.2 Derived Constructs
• 3.3.3 Data Structures
• 3.4 Conclusion
• Chapter 4 Minimal Model Semantics of MSVL
• 4.1 The Minimal Satisfaction Relation
• 4.2 Normal Form of Framed Programs
• 4.3 Existence Theorem of Minimal Models
• 4.3.1 Least Fixed Point Theorem
• 4.3.2 Existence Theorem
• 4.4 Examples
• 4.5 Conclusion
• Chapter 5 Operational Semantics of MSVL
• 5.1 Notation
• 5.2 Evaluation of Expressions
• 5.3 State Reduction
• 5.3.1 Semantic Equivalence Rules
• 5.3.2 Transition Rules within One State
• 5.3.3 Properties for State Reduction
• 5.4 Interval Reduction
• 5.5 Consistency between Minimal Model and Operational Semantics
• 5.5.1 Consistency for Finite Models
• 5.5.2 Consistency for Infinite Models
• 5.5.3 Nondeterministic Framed Programs
• 5.6 An Interpreter for MSVL
• 5.7 Conclusion
• Chapter 6 Axiomatic Semantics of MSVL
• 6.1 The Assertion Language
• 6.2 State Axioms and State Inference Rules
• 6.3 Axioms and Inference Rules over Intervals
• 6.4 Soundness and Completeness
• 6.4.1 Soundness
• 6.4.2 Completeness
• 6.5 Verification of Mutual Exclusion
• 6.6 Conclusion
• Chapter 7 Conclusions and Future Works
• 7.1 Conclusions
• 7.2 Future Works
• Acknowledgements
• References
• Finished Papers