基于B方法的嵌入式实时操作系统的设计

摘要	第1-5页
Abstract	第5-9页
第1章 绪论	第9-15页
·研究背景	第9-11页
·国内外研究现状	第11-12页
·论文的研究内容	第12-13页
·论文的内容组织	第13-15页
第2章 B方法	第15-32页
·B方法的介绍	第15-16页
·数学符号表示和广义代换语言	第16-19页
·数学符号表示	第16-18页
·广义代换语言	第18-19页
·抽象机	第19-23页
·抽象机的形式化描述	第20-22页
·抽象机的证明义务	第22-23页
·精化和实现	第23-26页
·REFINEMENT结构	第24-26页
·IMPLEMENTATION结构	第26页
·B方法的各种机器组织机制	第26-28页
·基于B方法的软件开发过程	第28-31页
·本章小结	第31-32页
第3章 一个嵌入式实时操作系统的形式化模型	第32-67页
·μC/OS-Ⅱ的介绍	第32-34页
·基于B方法的操作系统形式化模型fmC/OS设计	第34-66页
·任务管理	第35-40页
·任务的调度	第40-47页
·任务间的同步与通信	第47-55页
·内存管理	第55-61页
·机器OS	第61-63页
·机器的证明	第63-66页
·本章小结	第66-67页
第4章 fmC/OS模型的精化与实现	第67-86页
·精化	第67-68页
·任务管理的精化与实现	第68-78页
·规范OS的实现	第78-85页
·本章小结	第85-86页
总结与展望	第86-88页
总结	第86-87页
展望	第87-88页
参考文献	第88-91页
附录	第91-92页
致谢	第92页