从Murphi到Ocaml语言的编译器及其在模型检测中的应用

声明

致谢

摘要

1．1 研究背景及研究现状

1．2 本文的主要工作

1．3 论文的组织结构

2 背景知识

2．1 模型检测

2．2 模型检测语言Murphi和nuSMV

2．2．1 Murphi语言

2．2．2 nuSMV语言

2．3 Ocaml语言简介

2．4 编译器原理及工具

2．4．1 实现一个编译器的基本过程

2．4．2 Lex简介

2．4．3 Yacc简介

2．5 本章小结

3 编译器前端实现

3．1 Murphi词法分析及Lex构造

3．1．1 词法分析器构造

3．1．2 符号表定义

3．2 Murphi语法分析及Yacc构造

3．2．1 Yacc．y文件格式定义

3．2．2 抽象语法树定义与构造

3．3 本章小结

4 编译器后端实现

4．1 Ocaml语义模型定义

4．2 具体转换函数

4．3 实验

4．4 本章小结

5 编译器在模型检测中的应用

5．1 Murphi与nuSMV的建模能力

5．2 nuSMV转换器实现

5．3 转换结果

5．4 本章小结

6 结论

6．1 总结

6．2 工作展望

参考文献

附录

作者简历

学位论文数据集