从Murphi到Ocaml语言的编译器及其在模型检测中的应用
| 致谢 | 第5-6页 |
| 摘要 | 第6-7页 |
| ABSTRACT | 第7-8页 |
| 1 引言 | 第11-15页 |
| 1.1 研究背景及研究现状 | 第11-12页 |
| 1.2 本文的主要工作 | 第12-13页 |
| 1.3 论文的组织结构 | 第13-15页 |
| 2 背景知识 | 第15-26页 |
| 2.1 模型检测 | 第15页 |
| 2.2 模型检测语言Murphi和nuSMV | 第15-18页 |
| 2.2.1 Murphi语言 | 第15-17页 |
| 2.2.2 nuSMV语言 | 第17-18页 |
| 2.3 Ocaml语言简介 | 第18-19页 |
| 2.4 编译器原理及工具 | 第19-24页 |
| 2.4.1 实现一个编译器的基本过程 | 第19-21页 |
| 2.4.2 Lex简介 | 第21-23页 |
| 2.4.3 Yacc简介 | 第23-24页 |
| 2.5 本章小结 | 第24-26页 |
| 3 编译器前端实现 | 第26-44页 |
| 3.1 Murphi词法分析及Lex构造 | 第26-31页 |
| 3.1.1 词法分析器构造 | 第27-29页 |
| 3.1.2 符号表定义 | 第29-31页 |
| 3.2 Murphi语法分析及Yacc构造 | 第31-43页 |
| 3.2.1 Yacc.y文件格式定义 | 第32-34页 |
| 3.2.2 抽象语法树定义与构造 | 第34-43页 |
| 3.3 本章小结 | 第43-44页 |
| 4 编译器后端实现 | 第44-60页 |
| 4.1 Ocaml语义模型定义 | 第44-48页 |
| 4.2 具体转换函数 | 第48-55页 |
| 4.3 实验 | 第55-58页 |
| 4.4 本章小结 | 第58-60页 |
| 5 编译器在模型检测中的应用 | 第60-67页 |
| 5.1 Murphi与nuSMV的建模能力 | 第60-61页 |
| 5.2 nuSMV转换器实现 | 第61-64页 |
| 5.3 转换结果 | 第64-66页 |
| 5.4 本章小结 | 第66-67页 |
| 6 结论 | 第67-69页 |
| 6.1 总结 | 第67-68页 |
| 6.2 工作展望 | 第68-69页 |
| 参考文献 | 第69-72页 |
| 附录A 编译器后端转换函数 | 第72-74页 |
| 附录B nuSMV转换函数 | 第74-77页 |
| 作者简历 | 第77-79页 |
| 学位论文数据集 | 第79页 |
