FCS 优青论坛 | MSVL：一种类型化时序逻辑程序设计语言

导读

本篇「优青论坛」文章介绍了时序逻辑程序设计语言MSVL，并研究了如何在MSVL中将类型形式化并进行实施。「优青」作者为田聪。

田聪，西安电子科技大学教授。2013 年 NSFC“优秀青年科学基金”获得者。优青作者详细介绍参见后文。

MSVL 是一种时序逻辑程序设计语言，是投影时序逻辑（PTL）的可执行子集。MSVL 将系统的建模、仿真和验证三大功能集合于一体，是形式化验证的有力工具。在时序逻辑编程中，类型的开发是一个重要但具有挑战性的问题。本文研究了如何在 MSVL 中将类型形式化并进行实施。

文章使用了几组类型——基本数据类型、指针类型和结构类型对 MSVL 进行了扩展。对于每个类型，指定了数值的域，并根据逻辑函数和谓词定义了标准操作。然后，将程序变量类型声明和结构定义声明形式化为逻辑公式。文章还使用 MSVL 的建模、仿真和验证功能扩展了 MSV 工具包，从而对此理论研究进行了实施。通过在 AVL 树的构建和有序列表中的应用，表明了该语言的实用性。

FCS「优青论坛」由主编李未院士，执行主编熊璋教授和周志华教授发起，以综述论文的形式，集中展现「NSFC 优秀青年基金」获得者对所研究领域的分析和见解，介绍最新的研究进展和成果。

文 章 精 要

如需阅读本期推荐文章的全文，请点左下角的「阅读原文」链接。

作者介绍

田聪，西安电子科技大学教授、博导。主要研究方向包括可信嵌入式系统理论与技术、可信网络计算理论与技术、可信软件的基础理论与方法，已在重要学术期刊和会议上发表论文近70篇。承担了国家自然科学基金优秀青年基金项目、国家自然科学基金面上项目和国家自然科学基金青年基金项目。作为主要成员，参与了国家自然科学基金重点项目、国家重点基础研究发展计划973子课题、国家自然科学基金重大国际合作项目和可信软件重大专项培育项目。获“国家自然科学基金”优秀青年、教育部新世纪优秀人才、陕西省青年科技新星称号、陕西省科学技术二等奖1项。

相关文章

FCS 优青论坛 | 神经网络加速器研究综述

Zhen LI, Yuqing WANG, Tian ZHI, Tianshi CHEN

FCS 优青论坛 | 网络鲁棒性度量指标的比较研究

Jing LIU, Mingxing ZHOU, Shuai WANG, Penghui LIU

FCS 优青论坛 | 基于 Lyapunov 方法的线性时滞系统稳定性的研究综述

Jian SUN, Jie CHEN

FCS 优青论坛 | 整合癌症基因组学：计算模型、算法和数据分析

Jinyu CHEN, Shihua ZHANG

FCS 优青论坛 | 求解不适定问题的正则优化方法：综述及多目标框架

Maoguo GONG, Xiangming JIANG, Hao LI

FCS 优青论坛 | The role of prior in image based 3D modeling: a survey

Hao ZHU, Yongming NIE, Tao YUE, Xun CAO

FCS 优青论坛 | Recent progress & trends in predictive visual analytics

Junhua LU, Wei CHEN, Yuxin MA, Junming KE, Zongzhuang LI, Fan ZHANG, Ross MACIEJEWSKI

---

---

Frontiers of Computer Science

---

Frontiers of Computer Science 是由教育部主管、高等教育出版社和德国 Springer 公司共同出版的英文学术期刊。本刊于 2007 年创刊，双月刊，全球发行。主要刊登计算机科学领域具有创新性的综述论文、研究论文等。本刊主编为李未院士，执行主编为熊璋教授和周志华教授。编委会及青年 AE 团队由国内外知名学者及优秀青年学者组成。本刊被 SCI、Ei、DBLP、INSPEC、SCOPUS 和中国科学引文数据库（CSCD）核心库等收录，为 CCF 推荐期刊；两次入选“中国科技期刊国际影响力提升计划”；入选“第4届中国国际化精品科技期刊”。

---

长按二维码关注Frontiers of Computer Science公众号