可验证的数字机器

摘要	第1-3页
Abstract	第3-4页
中文文摘	第4-8页
第1章 绪论	第8-14页
·课题背景	第8-10页
·可视化图形建模	第10-11页
·形式化验证技术及其发展	第11-13页
·本文的主要内容	第13-14页
第2章 基于状态机的图形描述及其形式化	第14-24页
·状态机的图形表示及语法	第14-18页
·状态机的语义	第18-22页
·本章小结	第22-24页
第3章 扩展层次自动机	第24-32页
·扩展层次自动机的介绍	第24-26页
·扩展层次自动机的操作语义	第26-30页
·本章小结	第30-32页
第4章 基于状态机模型的验证方法	第32-48页
·状态机生成Büchi自动机	第32-38页
·描述模型的性质	第38-39页
·由线性时态逻辑公式生成Büchi自动机	第39-44页
·状态机的模型验证算法	第44-47页
·本章小结	第47-48页
第5章 验证优化与设计	第48-62页
·程序切片思想	第48页
·扩展层次自动机的切片准则	第48-52页
·扩展层次自动机切片的生成	第52-56页
·从性质公式中提取切片准则	第56-58页
·验证机器的设计思想及实例	第58-60页
·本章小结	第60-62页
第6章 总结	第62-64页
参考文献	第64-69页
攻读学位期间承担的科研任务与主要成果	第69-70页
致谢	第70-71页
个人简历	第71-72页