多类型时序逻辑程序设计

项目名称： 多类型时序逻辑程序设计

项目编号： No.61402347

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 赵亮

作者单位： 西安电子科技大学

项目金额： 26万元

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

中文关键词： 多类型；建模;仿真和验证语言；时序逻辑程序设计；形式语义；解释器

英文摘要： 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 prog

英文关键词： Many-Type；MSVL；Temporal Logic Programming；Formal Semantics；Interpreter