基于Event-B的软件形式化需求获取方法研究
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-9页 |
| 1 绪论 | 第9-16页 |
| ·软件建模方法概述 | 第9-13页 |
| ·统一建模语言(UML) | 第9-10页 |
| ·形式化方法 | 第10-13页 |
| ·现存问题及本文研究内容 | 第13-15页 |
| ·本文组织结构 | 第15-16页 |
| 2 基于公平扩充的离散系统模型 | 第16-25页 |
| ·离散系统概述 | 第16-19页 |
| ·复杂系统 | 第16-17页 |
| ·测试与模型推理 | 第17页 |
| ·基本离散系统模型 | 第17-19页 |
| ·基于公平扩充的离散系统模型 | 第19-24页 |
| ·程序的性质 | 第19-20页 |
| ·公平离散系统模型 | 第20-22页 |
| ·公平离散系统模型性质验证 | 第22页 |
| ·需求获取过程中复杂性控制方法 | 第22-24页 |
| ·需求模型复用 | 第24页 |
| ·小结 | 第24-25页 |
| 3 基于EVENT-B 的需求获取方法 | 第25-52页 |
| ·EVENT-B 的基本模型及其验证规则 | 第25-37页 |
| ·Event-B 模型基本结构 | 第25-28页 |
| ·Event-B 的广义代换 | 第28-30页 |
| ·Event-B 中前后谓词和广义代换的等价关系 | 第30页 |
| ·模型安全性证明义务产生规则 | 第30-31页 |
| ·模型活性证明义务产生规则 | 第31-36页 |
| ·模型基本结构的扩充及解释 | 第36-37页 |
| ·EVENT-B 模型的求精及其验证规则 | 第37-43页 |
| ·模型和场景求精 | 第37-39页 |
| ·内部事件求精 | 第39-42页 |
| ·外部事件求精 | 第42页 |
| ·合并事件 | 第42-43页 |
| ·求精过程中模型基本结构的扩充及解释 | 第43页 |
| ·一种新的模型分解方法 | 第43-49页 |
| ·模型分解的优点 | 第44页 |
| ·分解算法 | 第44-49页 |
| ·分解过程中模型基本结构的扩充及解释 | 第49页 |
| ·需求模型的复用策略 | 第49-51页 |
| ·从需求模型到程序 | 第51页 |
| ·小结 | 第51-52页 |
| 4 实例研究 | 第52-82页 |
| ·概述 | 第52-53页 |
| ·门禁系统概述 | 第52-53页 |
| ·需求书写风格 | 第53页 |
| ·门禁系统初步模型 | 第53-62页 |
| ·基本需求描述 | 第54-55页 |
| ·初始模型 | 第55-58页 |
| ·引入门票 | 第58-62页 |
| ·模型逐步求精与分解 | 第62-81页 |
| ·引入门禁控制端外设 | 第63-68页 |
| ·引入单片机 | 第68-74页 |
| ·引入中央计算机 | 第74-80页 |
| ·模型分解及其子模型求精 | 第80-81页 |
| ·小结 | 第81-82页 |
| 5 EVENT-B 的一种公平性扩充 | 第82-90页 |
| ·相关知识概述 | 第83-85页 |
| ·最弱前置条件和wlt | 第83页 |
| ·UNITY 中活性描述 | 第83-85页 |
| ·活性证明义务产生规则 | 第85-89页 |
| ·MP 公平 | 第86-88页 |
| ·弱公平 | 第88-89页 |
| ·下一步工作 | 第89-90页 |
| 6 结束语 | 第90-92页 |
| ·本文总结 | 第90-91页 |
| ·未来工作 | 第91-92页 |
| 参考文献 | 第92-97页 |
| 攻读硕士学位期间发表的论文目录、科研情况 | 第97-98页 |
| 致谢 | 第98页 |
