一个并发传值系统自动验证工具的图形界面实现
| 第一章 引言 | 第1-12页 |
| ·形式化方法及其背景 | 第6-7页 |
| ·模型检测 | 第7-9页 |
| ·模型检测工具 | 第9-11页 |
| ·已有模型检测工具介绍 | 第9-10页 |
| ·一个新的并发传值系统自动验证工具 | 第10-11页 |
| ·论文内容及组织 | 第11-12页 |
| ·论文的主要工作 | 第11页 |
| ·论文的组织 | 第11-12页 |
| 第二章 并发传值系统的模型及逻辑描述 | 第12-22页 |
| ·进程代数 | 第12-16页 |
| ·CCS与传值CCS | 第12-13页 |
| ·迁移系统 | 第13-16页 |
| ·逻辑描述 | 第16-22页 |
| 第三章 SML与C程序间的通信 | 第22-30页 |
| ·SML语言 | 第22页 |
| ·Motif | 第22-23页 |
| ·UNIX进程创建 | 第23页 |
| ·进程间通信 | 第23-28页 |
| ·管道通信 | 第24-25页 |
| ·套接字通信 | 第25-28页 |
| ·SML与C程序间的大型数据通信 | 第28-30页 |
| 第四章 工具图形界面的结构及实现 | 第30-41页 |
| ·图形界面的外观 | 第30页 |
| ·图形界面的功能 | 第30-31页 |
| ·图形界面与验证引擎的初始化 | 第31-33页 |
| ·窗口X事件处理 | 第33-35页 |
| ·主窗口菜单的实现 | 第35-36页 |
| ·正文部件的实现 | 第36页 |
| ·列表部件的实现 | 第36-37页 |
| ·按钮部件的实现 | 第37-38页 |
| ·DrawingArea部件的实现 | 第38-39页 |
| ·对话框的实现 | 第39-41页 |
| 第五章 图形界面与验证引擎的交互 | 第41-63页 |
| ·验证引擎的Command Loop | 第41-46页 |
| ·Command Loop对验证命令请求的解码 | 第41页 |
| ·Load命令请求 | 第41-42页 |
| ·Bisimulation命令请求 | 第42页 |
| ·ModelCheck命令请求 | 第42页 |
| ·Simulation命令请求 | 第42-45页 |
| ·Move命令请求 | 第45-46页 |
| ·ModEnv命令请求 | 第46页 |
| ·验证任务的交互实现 | 第46-63页 |
| ·图形界面对验证命令请求的编码 | 第46-47页 |
| ·系统描述文件的编译 | 第47-48页 |
| ·系统进程的定义表达式显示 | 第48-49页 |
| ·互模拟等价关系验证 | 第49-50页 |
| ·模型检测及反例的图形显示 | 第50-55页 |
| ·系统仿真 | 第55-63页 |
| 第六章 结束语 | 第63-64页 |
| 参考文献 | 第64-66页 |
| 在学期间发表论文 | 第66-67页 |
| 致谢 | 第67页 |
