资源描述：
《uml状态图到形式化b语言转换的实例研究》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、UML状态图到形式化B语言转换的实例研究第7卷第24期2007年l2月1671?-1819(2007)24..6334.?06科学技术与工程ScienceTechnologyandEnglneefingV01.7No.24Dee.20o7@2007Sei.Teeh.Engng.UML状态图到形式化B语言转换的实例研究邹盛荣孟静阳雪平腾腾陈字孙建国(扬州大学信息工程学院,扬州225009)摘要使用UML中的状态图可以帮助描绘生物领域中碰到的很多问题,而形式化B方法能为生物系统建模并提供严格的证明,UML
2、和B的结合可产生一种形式化的UML,并精确地用B方法建模.对免疫因子网络中T细胞免疫状态的UML状态图进行了两种方法的形式化,并进行了比较.关键词UML状态图形式化方法B方法T细胞中图法分类号'rP311;文献标识码A统一建模语言UML已经成为面向对象软件系统中描述分析和设计阶段模型的标准化记法.用图表来描述模型是非常容易理解的.开发人员及其用户能直观地抓住一个模型的大致结构,因此为系统条件的讨论和可能的实现建立了一个良好的基础.计算机被越来越多地用于解决那些故障可能会导致严重后果(包括危及生命)的任
3、务.计算机在控制宇宙飞船,航天器,火车,汽车,核反应堆和医疗设备等等的应用中起着至关重要的作用.在这些系统中,确保计算机系统的完全可靠至关重要.提高计算机软件可靠性的一种重要技术是使用形式化方法(FormalMethods).近年来,国外对形式化方法在软件开发中的应用作了大量的研究与实践工作,形式化方法已不再只是一种研究所里的学术研究工作,而是已经开始被工业界接受,并应用于开发实际的系统.国处已有包括形式化方法,形式化语言和形式化工具在内的比较成熟的形式化系统,如VDM2007年9月6日收到江苏省自然
4、科学基金项目(BK2004052)和扬州大学自然科学基金项目(KK0513109)资助第一作者简介:邹盛荣(1968一),男,江苏省高邮人,扬州大学信息工程学院副教授,研究方向:软件工程,B语言与方法.通信作者简介:孟静(1983一),女,江苏省常州市,扬州大学信息工程学院硕士生,研究方向:领域为软件工程与B形式化方法.E—mail:zlmj1983@sohu.corn;mengjingbbn@163corn.系统,z系统.为了保证软件产品的可靠性,规格说明应具有可理解性和精确性,这是程序实现的基本保
5、证.形式化的规格说明语言避免了自然语言的歧义性和不精确性,奠定了保证程序的正确性的各种形式化方法的基础.因此,将形式化的理论和方法用于需求分析与规格说明极为必要,也是实现软件自动化生产的根本前提.生物系统是一个复杂的反应系统,免疫系统是保护我们机体免受外来抗原和异物侵害的保护系统,它是通过分泌多种分子信号及因子进行自我调节的.凡是由免疫细胞发挥效应以清除异物的过程称为细胞免疫,参与作用的细胞称为免疫效应细胞,细胞免疫是由T细胞介导的.一个活动的细胞可以看成是内部状态转换的一个系统,反映了细胞在特定环境
6、下的交互过程.这些内部状态的转换是由环境给予细胞的因子信号触发的.比如,一个初始T细胞如果不分化,可以存活很多年,这些初始细胞循环往复地从血液进入淋巴器官,最后再回到血液来侦察身体中可能会出现的变化.这个发现过程是由T细胞和抗原递呈细胞协助交互完成的,当特定的抗原递呈细胞停止移动时,初始T细胞可以识别其表面的特异性抗原,再开始活化,增殖,并且分化成起警卫作用的效应T细胞.24期邹盛荣,等:UML状态图到形式化B语言转换的实例研究6335关于细胞免疫T细胞的行为,传统的描述方法是把一个细胞看成一个黑盒¨
7、J,因此它只能说明在给定条件下细胞会产生哪些反应,而不能说明这些输入条件是怎样转化成输出的,信号的转变过程被忽视了.因此,为了更好地理解更低层次上的行为,我们必须能"放大"整个系统,更细致,更精确地描述其内部的活动.用UML的状态图就能完整并直观地描述这些活动,但是UML还缺乏形式上的精确语义J.相比之下,B语言精确地提供了需求描述并严格的证明.本文对描述免疫因子网络中T细胞行为的UML状态图进行形式化,并用抽象机器语言来完整地描述这个模型.1UML和B方法介绍l-lUMLUML是对软件系统中的制品进
8、行可视化,详述,构造和文档化的语言.定义中所说的制品是指软件开发过程中产生各种各样的产物,如模型,源代码,测试用例等J.UML的状态图主要用于描述一个对象在其生存期间的动态行为J,表现一个对象所经历的状态序列,引起状态转移的事件,以及因状态转移而伴随的动作;是UML中对系统的动态行为建模图形之一,状态图在检查,测试和描述类的动态行为时非常有用.1.2B方法形式化方法表示利用数学的方法——集合论和一阶逻辑的思想J,来对软件进行规格说明,设计和实现,这样软件
