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

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

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

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 本文工作
第二章 相關(guān)知識(shí)介紹
    2.1 引言
    2.2 Event-B介紹
    2.3 Event-B抽象模型的組成部分
        2.3.1 靜態(tài)部分
        2.3.2 動(dòng)態(tài)部分
        2.3.3 Context和Machine的關(guān)系
    2.4 Rodin平臺(tái)
    2.5 本章小結(jié)
第三章 Event-B與B方法在免疫系統(tǒng)中的比較研究
    3.1 引言
    3.2 B方法
        3.2.1 B方法開發(fā)過程
        3.2.2 B方法的優(yōu)缺點(diǎn)
    3.3 Event-B與B方法的比較
    3.4 針對(duì)免疫系統(tǒng)需求的Event-B的優(yōu)勢(shì)
        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模型驗(yàn)證
    5.1 引言
    5.2 證明義務(wù)的生成
    5.3 證明器
    5.4 自動(dòng)證明
    5.5 交互式證明
    5.6 本章小結(jié)
第六章 總結(jié)與展望
    6.1 總結(jié)
    6.2 展望
參考文獻(xiàn)
致謝
論文發(fā)表情況及參加科研項(xiàng)目、學(xué)術(shù)會(huì)議



本文編號(hào)：3797701