在當(dāng)今社會中,社會信息化高速發(fā)展,每一個行業(yè)都與軟件緊密相關(guān)。在開發(fā)一個軟件時,首先要做的是對軟件需求進行分析,而在這個分析描述的過程中又避免不了因語法或語義帶來的錯誤。為了減輕這些不必要的錯誤帶來的損失,形式化方法應(yīng)運而生。目前形式化方法領(lǐng)域中,比較常見的兩種方法是B方法和Event-B方法,Event-B方法由B方法演化而來,具有許多B方法沒有的優(yōu)點,并且Event-B方法在工具平臺上有著很大的優(yōu)勢。Rodin平臺是基于Eclipse開發(fā)的集成環(huán)境,為Event-B方法提供了系統(tǒng)級的開發(fā)模式,可以通過逐層精化的方式為模型添加所需的屬性和功能,并且Rodin平臺簡化了 Event-B方法的驗證過程,提供了多種自動證明器,支持更多的證明義務(wù),為模型的精化和證明提供了有效的支持,同時最小化對更改現(xiàn)有證明的影響,在軟件開發(fā)的前期就保證了軟件模型的正確性和一致性。本文以免疫系統(tǒng)作為開發(fā)需求,使用Event-B方法建立免疫系統(tǒng)抽象模型,并詳細闡述在Rodin平臺下對該模型從需求分析到驗證的全部過程,主要開展了如下工作:(1)研究了現(xiàn)階段常用的形式化方法B方法與Event-B方法各自的建模方式,...

【文章頁數(shù)】：79 頁

【學(xué)位級別】：碩士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 本文工作
第二章 相關(guān)知識介紹
    2.1 引言
    2.2 Event-B介紹
    2.3 Event-B抽象模型的組成部分
        2.3.1 靜態(tài)部分
        2.3.2 動態(tài)部分
        2.3.3 Context和Machine的關(guān)系
    2.4 Rodin平臺
    2.5 本章小結(jié)
第三章 Event-B與B方法在免疫系統(tǒng)中的比較研究
    3.1 引言
    3.2 B方法
        3.2.1 B方法開發(fā)過程
        3.2.2 B方法的優(yōu)缺點
    3.3 Event-B與B方法的比較
    3.4 針對免疫系統(tǒng)需求的Event-B的優(yōu)勢
        3.4.1 免疫系統(tǒng)需求描述
        3.4.2 模型結(jié)構(gòu)
        3.4.3 精化方式
        3.4.4 無死鎖性
        3.4.5 證明方式
        3.4.6 工具的支持
    3.5 本章小結(jié)
第四章 基于Event-B的免疫系統(tǒng)模型
    4.1 引言
    4.2 Event-B的建模過程
    4.3 抽象模型
    4.4 模型精化
        4.4.1 第一次精化
        4.4.2 第二次精化
        4.4.3 第三次精化
    4.5 本章小結(jié)
第五章 Event-B模型驗證
    5.1 引言
    5.2 證明義務(wù)的生成
    5.3 證明器
    5.4 自動證明
    5.5 交互式證明
    5.6 本章小結(jié)
第六章 總結(jié)與展望
    6.1 總結(jié)
    6.2 展望
參考文獻
致謝
論文發(fā)表情況及參加科研項目、學(xué)術(shù)會議



本文編號：3797701