MSVL编译器中建模方法的研究与实现

摘要

随着计算机在人类社会各个领域的普及，软硬件系统的正确性问题已经备受关注，在过去的几十年里，形式化验证方法已成为保障软硬件系统正确性的重要途径。其中，时序逻辑由于其简洁和无二义的特性，已经被广泛的应用于形式化验证中。
　　作为一种时序逻辑程序设计语言，MSVL是投影时序逻辑（PTL）的一个可执行子集，可用于对软硬件系统进行仿真、建模以及验证。其中，建模功能作为验证的基础，是MSVL语言中极其重要的一部分。
　　程序设计语言的实现工具主要包括编译器与解释器。其中，编译器的运行速度与内存占用率均优于解释器。本文主要研究如何在编译器结构下为MSVL程序建立模型。MSVL程序模型的建立，一方面以图的形式呈现出程序的执行流程，简单明了；另一方面，模型可以更精准地刻画出程序中的状态迁移，便于后续验证工作的开展。
　　本文的主要贡献在于提出了建模方法的设计框架，并解决了该框架在实现中的关键问题。该框架借助于LLVM编译系统平台，基于MSVL语义，将MSVL语句转化为中间代码（IR）并引入动态控制机制，随后经由链接器生成可执行文件，最终得到程序模型。在框架实现过程中，针对 MSVL程序的特点，提出了四种关键技术，包括时序性质的体现、多路径程序的执行、MSVL特有语句的实现以及程序模型的绘制。最后，本文介绍了MSVL建模工具的使用方法，并给出了对经典问题建模的示例，验证了建模框架的可行性。

目录

声明

插图索引

表格索引

缩略语对照表

第一章 绪论

1.1研究背景

1.2形式化方法

1.3时序逻辑

1.4研究目的及论文组织结构

第二章 相关理论与技术

2.1 LLVM编译系统

2.2投影时序逻辑

2.3 MSVL

第三章 建模方法的设计框架

3.1编译器

3.2建模的框架

3.3本章小结

第四章 建模框架实现时的关键问题

4.1建模框架中的难点分析

4.2时序性质的体现

4.3多路径的实现

4.4 MSVL部分语句的实现

4.5绘制模型功能的实现

4.6本章小结

第五章 建模工具介绍及运行示例

5.1建模工具的使用

5.2程序建模示例

5.3本章小结

第六章 总结与展望

6.1总结

6.2展望

参考文献

致谢

作者简介