基于Petri网的嵌入式系统建模与验证研究

摘要	第1-4页
ABSTRACT	第4-7页
第一章 绪论	第7-10页
·研究背景	第7页
·研究现状	第7-8页
·本文的研究工作及其意义	第8-9页
·本文的基本结构	第9-10页
第二章 嵌入式系统的模型概述	第10-17页
·嵌入式系统的特点	第10页
·嵌入式系统的设计流程	第10-12页
·嵌入式系统建模的常用方法	第12-16页
·有限状态机	第12-13页
·状态图表	第13-14页
·数据流图	第14-15页
·Petri 网	第15-16页
·本章小结	第16-17页
第三章 基于PRES+的实时嵌入式系统建模	第17-37页
·基本 Petri 网	第17-18页
·基本PRES+模型	第18-23页
·PRES+的基本定义	第18-19页
·PRES+的功能性描述	第19-20页
·PRES+的动态行为描述	第20-23页
·PRES+的等价和分层概念	第23-30页
·PRES+的等价概念	第23-25页
·等级 PRES+模型	第25-29页
·建模实例	第29-30页
·PRES+的组合与修改操作	第30-36页
·网加和网减运算	第30-34页
·组合与修改的建模实例	第34-36页
·本章小结	第36-37页
第四章 PRES+模型的分析与验证	第37-66页
·PRES+模型的分析	第37页
·形式化验证方法	第37-49页
·时间自动机	第37-38页
·验证工具 UPPAAL	第38-41页
·PRES+模型到TA 模型的转换	第41-44页
·铁路岔口问题	第44-49页
·动态行为的模拟	第49-57页
·普通Petri 网动态行为的模拟	第49-52页
·PRES+动态行为的模拟	第52-57页
·简化PRES+模型	第57-64页
·本章小结	第64-66页
总结与展望	第66-67页
致谢	第67-68页
参考文献	第68-72页
附录：作者在攻读硕士学位期间发表的论文	第72页