多类型时序逻辑程序设计

Temporal logic programming is currently one of the most widely used programming paradigms, and it has great significance for program verification. This project proposes research on many-type temporal logic programming, so as to enhance temporal logic programming in its functionality and applicability. For this, we propose to introduce the notion of type and define multiple types on the basis of Modelling, Simulation and Verification Language (MSVL), obtaining Many-Type MSVL, a many-type temporal logic programming language. We plan to study its type system, model semantics, operational semantics, axiomatic semantics, type safety, and equivalence between different semantics. In addition, we are going to develop an interpreter for Many-Type MSVL, implementing the type checking, modelling, simulation and verification of many-type temporal logic programs.

时序逻辑程序设计是目前一种广泛使用的程序设计模式，对程序验证具有重要的意义。本项目拟研究多类型时序逻辑程序设计，以加强时序逻辑程序设计的功能和适用性。为此，我们在建模、仿真和验证语言（MSVL）的基础上引入类型的概念，并定义多种类型，得到一种多类型时序逻辑程序设计语言：多类型MSVL。研究多类型MSVL的类型系统、模型语义、操作语义、公理语义、类型安全性和语义之间等价性。开发多类型MSVL的解释器，实现对多类型时序逻辑程序的类型检查、建模、仿真和验证。

时序逻辑程序设计是目前一种广泛使用的程序设计模式，对程序验证具有重要的意义。现有的时序逻辑程序设计语言注重在逻辑方面的功能，然而在类型方面的功能有限，往往仅支持单一类型。本项目对建模、仿真和验证语言MSVL进行扩展，使用投影时序逻辑PTL定义了整型、浮点型、字符型、数组、列表、指针、结构等多种类型以及各类型的相关操作，得到了一种多类型的时序逻辑程序设计语言。构建了多类型MSVL的形式语义理论体系，以极小模型的方式定义了该语言的模型语义，以格局约简的方式定义了该语言的操作语义，并证明了这两种语义的等价性。研究了基于PTL的程序验证理论，提出了相应的模型检测方法和运行时验证方法。作为理论的实现，开发出多类型MSVL的解释器工具，具备对多类型时序逻辑程序的建模、仿真与验证功能。作为理论和工具的应用，实现了一种基于多类型MSVL的社交网络系统验证方法，并使用该方法验证了社交网络系统中若干条关于隐私策略和用户关系强度的性质。本项目对多类型MSVL的开发与研究改进了目前国内外时序逻辑程序设计语言缺乏多类型支持这一不足，增强了时序逻辑程序设计的功能和适用性。