UML状态图到形式化B语言转换的实例研究  

Case Study:Translation of the UML Statecharts in to Formal B Language

作　　者：邹盛荣[1] 孟静[1] 阳雪平[1] 腾腾[1] 陈宇[1] 孙建国[1] 

机构地区：[1]扬州大学信息工程学院,扬州225009

出　　处：《科学技术与工程》2007年第24期6334-6338,6343,共6页Science Technology and Engineering

基　　金：江苏省自然科学基金项目(BK2004052);扬州大学自然科学基金项目(KK0513109)资助

摘　　要：使用UML中的状态图可以帮助描绘生物领域中碰到的很多问题,而形式化B方法能为生物系统建模并提供严格的证明,UML和B的结合可产生一种形式化的UML,并精确地用B方法建模。对免疫因子网络中T细胞免疫状态的UML状态图进行了两种方法的形式化,并进行了比较。The use of statecharts in UML can help confronting many questions in the field of biology, while the B method, one of the formal methods, can construct models for biological system, and produce rigorous proof obligations. The combination of UML and B can provide a formulized UML, and found models with B method accurately. This paper introduces two methods which are used to translate the statechart of the behaveior of T cell in the immune cytokine networks in to B machines, and gives the comparison of them.

关 键 词：UML 状态图 形式化方法 B方法 T细胞 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]