基于Event-B形式化方法的免疫系统模型研究

发布时间：2023-04-22 13:10

　　在当今社会中,社会信息化高速发展,每一个行业都与软件紧密相关。在开发一个软件时,首先要做的是对软件需求进行分析,而在这个分析描述的过程中又避免不了因语法或语义带来的错误。为了减轻这些不必要的错误带来的损失,形式化方法应运而生。目前形式化方法领域中,比较常见的两种方法是B方法和Event-B方法,Event-B方法由B方法演化而来,具有许多B方法没有的优点,并且Event-B方法在工具平台上有着很大的优势。Rodin平台是基于Eclipse开发的集成环境,为Event-B方法提供了系统级的开发模式,可以通过逐层精化的方式为模型添加所需的属性和功能,并且Rodin平台简化了 Event-B方法的验证过程,提供了多种自动证明器,支持更多的证明义务,为模型的精化和证明提供了有效的支持,同时最小化对更改现有证明的影响,在软件开发的前期就保证了软件模型的正确性和一致性。本文以免疫系统作为开发需求,使用Event-B方法建立免疫系统抽象模型,并详细阐述在Rodin平台下对该模型从需求分析到验证的全部过程,主要开展了如下工作:(1)研究了现阶段常用的形式化方法B方法与Event-B方法各自的建模方式,...

【文章页数】：79 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 研究背景
    1.2 国内外研究现状
    1.3 本文工作
第二章 相关知识介绍
    2.1 引言
    2.2 Event-B介绍
    2.3 Event-B抽象模型的组成部分
        2.3.1 静态部分
        2.3.2 动态部分
        2.3.3 Context和Machine的关系
    2.4 Rodin平台
    2.5 本章小结
第三章 Event-B与B方法在免疫系统中的比较研究
    3.1 引言
    3.2 B方法
        3.2.1 B方法开发过程
        3.2.2 B方法的优缺点
    3.3 Event-B与B方法的比较
    3.4 针对免疫系统需求的Event-B的优势
        3.4.1 免疫系统需求描述
        3.4.2 模型结构
        3.4.3 精化方式
        3.4.4 无死锁性
        3.4.5 证明方式
        3.4.6 工具的支持
    3.5 本章小结
第四章 基于Event-B的免疫系统模型
    4.1 引言
    4.2 Event-B的建模过程
    4.3 抽象模型
    4.4 模型精化
        4.4.1 第一次精化
        4.4.2 第二次精化
        4.4.3 第三次精化
    4.5 本章小结
第五章 Event-B模型验证
    5.1 引言
    5.2 证明义务的生成
    5.3 证明器
    5.4 自动证明
    5.5 交互式证明
    5.6 本章小结
第六章 总结与展望
    6.1 总结
    6.2 展望
参考文献
致谢
论文发表情况及参加科研项目、学术会议



本文编号：3797701