基于Event-B的免疫系统设计与开发

发布时间：2020-05-11 15:28

【摘要】：随着计算机软件系统规模的日益庞大,系统的复杂性也在不断提升,设计中存在的潜在问题将会影响到软件系统的安全性和可靠性。传统的软件工程方法已经很难满足目前复杂和安全性都要求极高的需求,迫切需要更适应当前发展需求的方法来开发安全性更高的软件和成本较低的大型复杂系统。为了解决上述问题,统一建模语言(UML)在软件开发设计中被广泛应用,UML是一种半形式化的图形建模语言,它使用清晰直观的图形对系统进行描述,得到的图形化软件规约便于沟通和理解,现已在面向对象分析和设计中成为软件业界的标准。但是,UML的语义部分采用的是非形式化的自然语言缺乏精确的语义,导致对复杂的大型软件系统的描述不够精确,容易产生模糊性和二义性,不便于使用者建立严格的需求模型以及不便于使用自动化工具对所描述的规约进行一致性检查、分析和验证。形式化方法和UML二者之间存在很大的互补性,形式化方法严格的数学定义恰好能在语义方面弥补UML的不足,能够对UML建模结果与需求描述进行一致性检查和正确性分析。同时,UML能够降低直接使用形式化方法进行系统开发的难度,增强了形式化方法在系统开发中的实际应用价值。将UML和形式化方法结合起来,对提高软件的可靠性和安全性有着极其重要的意义。为了能够在开发中及时发现错误并改正,降低开发成本,精确、简明地验证和规范软件系统和性质,在分析UML模型图特点的基础上,本文选择Event-B形式化方法作为复杂非线性的免疫系统UML模型图的形式规约方法,主要工作如下:1.简述了 UML的基本概念和常被用于解决面向对象建模问题的应用背景,介绍了 UML便于沟通和支持软件开发整个生命周期的优点,并指出UML缺乏精确的语义定义,对软件结构的描述只能停留在非形式化的层次上。针对这个问题,本文提出将Event-1β形式化方法与UML相结合,Event-B方法以其严谨的数学理论基础弥补UML的非形式化语义定义,并且Event-B方法的Rodin工具自带证明义务自动生成器可以为模型自动生成证明义务弥补了 UML模型图缺少验证工具的问题。2.研究了免疫系统在机体内的运行机制,获取要建立模型的需求,利用UML建立清晰直观的模型图,从系统的静态和动态两方面入手详细描述免疫系统功能。采用Event-B方法对模型进行形式化分析和规约,并制定精化策略为免疫系统添加行为规则和完善功能。通过Event-B形式化方法的模型检测和定理自动证明来保证免疫系统与需求的一致性和正确性,从而提升免疫系统的可靠性。3.根据UML和Event-B模型对系统的建模、分析和验证,利用Java编程语言将经过UML和Event-B形式化方法设计免疫系统转化为可执行代码,并将流感病毒的相关参数设定到免疫系统中。运行所建立的免疫系统后,系统将生成参与细胞的运动和细胞碰撞图,并显示每种细胞的实时数量曲线图。系统运行后所得的实验结果与生物学免疫应答规律进行比较可以发现其规律是一致的,验证了所开发的免疫系统的合理性。
【图文】：

８逦扬州大学硕士学位论文逦逡逑四、用户模型层逡逑用户模型层通常又称为Ｍ０层，，它位于所有层次的最底部，该层的每个实例都是模型逡逑层和元模型层概念的实例。该抽象级别的模型通常叫作对象或实例模型，用户模型层的主逡逑要作用是描述一个特定的信息。逡逑２．１．４邋ＵＭＬＪｉＭＸ＾：邋ＥＡ逡逑ＥＡ邋（Ｅｎｔｅｒｐｒｉｓｅ邋Ａｒｃｈｉｔｅｃｔ）是一个对于软件系统开发有着极好支持的计算机辅助软件工逡逑程软件。ＥＡ不同于普通的ＵＭＬ画图工具，它支持软件开发的整个生命周期。在需求分析逡逑阶段，系统分析与设计阶段，系统开发及部署等方面有着强大的支持，同时加上对多种编逡逑程语言的正逆向工程，项目管理，文档生成，数据建模等方面。可以让系统开发中各个角逡逑色都获得最好的开发效率。图２．３－２．５为使用ＥＡ建立ＵＭＬ用例、类和其他模型图。逡逑＇

蒋思萍基于Ｅｖｅｎｔ－Ｂ的免疫系统设计与开发逦逡逑：：二－．二：：二＿＿二＿？＿１＿逦Ｖ逦＂逦＇邋■邋－Ｊ；逦－邋Ｖ邋—邋？＿N二＿—逦逦逦…一逦－－逡逑，ａ邋：■逦－ｉ邋？，；ｊ邋ａｉ邋ａ邋？／．．邋ａａ；逦－逡逑
【学位授予单位】：扬州大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：TP311.52

【相似文献】

相关期刊论文 前10条

1 傅育熙;李国强;田聪;;形式化方法的理论基础专题前言[J];软件学报;2018年06期

2 ;《软件学报》形式化方法的理论基础专刊征文通知[J];软件学报;2017年03期

3 ;《软件学报》软件形式化方法与应用专刊征文通知[J];软件学报;2015年06期

4 彭成;王盼卿;;软件形式化开发方法的选择策略研究[J];电子设计工程;2014年15期

5 王戟;李宣东;;形式化方法与工具专刊前言[J];软件学报;2011年06期

6 吕建强;夏春芬;;形式化方法在密码协议中的应用[J];科技信息;2009年06期

7 姜利;孙永强;;形式化方法的发展及展望[J];计算机科学;1998年02期

8 柴振荣;形式化方法与软件的可靠性[J];管理科学文摘;1999年09期

9 郑士贵;智能服务网络形式化方法的模拟和实质[J];管理科学文摘;1997年01期

10 郑红军;张乃孝;;软件开发中的形式化方法[J];计算机科学;1997年06期

相关会议论文 前6条

1 王梓;付建苏;刘海天;张民强;陈阳;;面向同步语言的多时钟系统行为建模与验证[A];第六届中国指挥控制大会论文集（下册）[C];2018年

2 高静;曹子宁;;基于空间逻辑和计算树逻辑的模型检测[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

3 任雁;田婕;孙辉;周永;;混成系统测试研究综述[A];2011年通信与信息技术新进展——第八届中国通信学会学术年会论文集[C];2011年

4 ;基于时间自动机的实时系统建模及验证[A];第六届和谐人机环境联合学术会议（HHME2010)、第19届全国多媒体学术会议（NCMT2010）、第6届全国人机交互学术会议（CHCI2010）、第5届全国普适计算学术会议（PCC2010）论文集[C];2010年

5 刘润杰;申金媛;穆维新;;形式化开发非递归Koch曲线算法[A];计算机研究新进展（2010）——河南省计算机学会2010年学术年会论文集[C];2010年

6 张沫;沈苏彬;;基于万维网服务的电信开放组合业务:研究综述[A];中国通信学会信息通信网络技术委员会2005年年会论文集[C];2005年

相关重要报纸文章 前2条

1 上海交通大学APEX数据和知识管理实验室 王昊奋邋俞勇;语义Web推动下一代搜索[N];计算机世界;2007年

2 天津市第一中级人民法院 李宝明;论法官的思维[N];天津日报;2008年

相关博士学位论文 前10条

1 郑长宗;安全苛求通信系统的形式化建模及验证[D];中国铁道科学研究院;2011年

2 方徽星;基于协同验证与混成关系的混成系统形式化分析验证[D];华东师范大学;2016年

3 张涛;复杂信息系统模型的形式化验证方法研究[D];哈尔滨工程大学;2012年

4 盖新貌;终端信任链理论模型及其实现机制研究[D];国防科学技术大学;2013年

5 张鹏;形式化方法在云计算中的应用研究[D];吉林大学;2014年

6 张健;Agent角色模型与多agent系统构造方法研究[D];山东大学;2012年

7 艾萍;构件柔性组装描述的形式化方法研究及其在水利领域的应用[D];河海大学;2002年

8 徐丙凤;构件化嵌入式软件安全性分析方法研究[D];南京航空航天大学;2014年

9 祝义;嵌入式软件需求规约到软件体系结构模型的转换研究[D];南京航空航天大学;2011年

10 黄滟鸿;面向实时嵌入式系统的中断语义理论研究[D];华东师范大学;2014年

相关硕士学位论文 前10条

1 蒋思萍;基于Event-B的免疫系统设计与开发[D];扬州大学;2018年

2 王建斌;基于Event-B的矿井机车运行过程控制的建模与验证研究[D];合肥工业大学;2017年

3 陈姣;战场数据样本空间形式化描述与样本生成[D];南京大学;2018年

4 顾海博;操作系统全局性质的形式化描述和验证[D];中国科学技术大学;2018年

5 付凯明;碘[~(125)I]自动化生产线控制程序的设计及其形式化方法验证[D];北京工业大学;2016年

6 朱蕾儿;面向基本蚁群算法的形式化研究[D];北京化工大学;2017年

7 刘中军;基于形式化方法的SIP研究与应用[D];北京邮电大学;2006年

8 游颖;算法形式化方法在三类组合数学问题求解中的应用研究[D];江西师范大学;2017年

9 施炜;PAR方法应用于管理信息系统开发方法的初步研究[D];江西师范大学;2004年

10 闵洪军;软件工程中形式化方法研究[D];浙江大学;2006年

本文编号：2658671