B方法在流感病毒入侵免疫系统模型设计中的应用

摘要：在我们的工作中，B方法已被用在一些极其重要的软件项目中并获得了很大成功。其中有不少应用于生物学方面的成功范例，我们用B方法建立了流感病毒入侵免疫系统因子网络的形式化模型，利用了生物信息学的理念，把免疫系统当成一个网络化的分布式信息系统来研究，以期望通过这样的研究为感疫苗研制、流感诊断和免疫疗法研究提供帮助。

关键词：B方法；流感病毒；模型设计

中图分类号：TP311文献标识码：A文章编号：1009-3044(2007)18-31646-02

The Flue Virus Invades a Formal B Method Model Design of Immune System

TANG Yu1,2,ZOU Sheng-rong1

(1.College of Information Engineering,Yangzhou University,Yangzhou 225009,China;(2.Taizhou Normal College,Taizhou 225300,China)

Abstract:In our works, the B method has already been used in some very and important software items and acquired very successful.There aren't a few successful examples which apply in the biology among them, we built up flue virus to invade immune system factor the formal models of the network with the B method, making use of a living creature information to learn of principle, be turned as a network the immune system of the distributes type information system to study, with the expectation pass thus of research for the feeling vaccine develop, flue diagnosis and immunity therapy research provide a help.

Key words:B method;Flue virus;Model design

1 引言

B语言与方法是一种支持从规格说明到代码生成整个开发过程的形式化方法。它使用相对简单且为人们所熟悉的集合符号表示法来描述抽象机的状态变换，从抽象机开始，逐步精化，直到最后的实现程序。

目前，流感病毒入侵免疫系统是生物上研究的一个热点，但同时也是一个难点。一方面，虽然有不少人在这方面进行过大力地探索，取得了不少的研究成果，但还是存在着许多问题。这些成果中虽然发现了不少和流感病毒入侵后有关的细胞因子，并对其作用进行过深入的研究，但还是无法明确细胞因子在其作用过程中到底是如何作用的，有的只知道该细胞因子的生物作用，知道其作用结果，这对于流感病毒入侵免疫系统的研究还远远不够。所以，我们何不想想用计算机的方法来模拟因子的作用，以便从中发现其规律呢？

B方法已被用在一些极其重要的软件项目中并获得了很大成功。其中有不少应用于生物学方面的成功范例，所以本论文将以B方法来实现流感病毒入侵免疫系统的一个难题。

2 流感病毒入侵免疫系统的建模

以下是我们根据流感病毒入侵免疫系统中几种常见免疫细胞与免疫因子的功能以及它们之间的相互作用，而最终得出一个因子网络调控图（见下图 ）。

图中由四部分组成：流感病毒、细胞，细胞因子，抗原。它们之间相互发生作用，图中各细胞因子的分泌源、作用对象以及它在模型中模拟的作用功能的描述如下：

3 流感病毒入侵免疫系统的因子网络的形式化B模型

3.1系统分析

该程序的目的是模拟流感病毒入侵免疫系统因子网络调控图的运行过程，观察其运行过程中各种量的变化，以及该调控图的稳定状态如何，各种初始条件对其有什么样的影响。为了精确地描述该程序，我们用形式化语言B来对其进行形式化描述。根据程序中所涉及的实体，我们可以分为：流感病毒、细胞、因子、抗原、抗体五个实体，在Ｂ方法中用五种抽象机描述。

3.2 系统的B方法描述

3.2.1机器Ｃell

这个机器可以封装细胞类，这里要定义三个集合，第一个集合是CELL，它是一个延期集合，表示现在的或将来的细胞。第二个集合是CATEGORY，表示细胞的不同类别。第三个集合是STATUS，表示细胞所处的状态。

3.2.2机器cytokine

与前面的Cell机器类似，Cytokine封装细胞因子的各种属性及操作。这里定义两个集合，一个延期集合CYTOKINE，一个种类集合CATEGORY。由于该机器要引用机器Ｃell中的变量，所以必须将它包含进来。其中种类集合CATEGORYK中含有九种细胞因子IL-1,IL-2,IL-4,IL-6,IFN-α,IFN-β,IFN-γ,TNF-R1,M-CSF。

3.2.3机器FuleVirus

FuleVirus机器与前面的Cell机器类似，FuleVirus封装了抗原的各种属性及操作。这只定义一个集合，VIRUS。

3.2.4机器antibody

Antibody机器封装了抗体的各种属性及操作。这只也定义一个集合，ANTIBODY。

4 系统模拟

4.1系统设计

4.1.1设计思想

首先定义对象管理类、用来管理各种对象，包括:流感病毒、细胞、细胞因子、抗原及抗体。然后定义一个动画控制类，用于衔接对象管理类和图形界面，将其状态显示到图形界面上。图形界面中可以设置对象的参数和全局设置，图形界面中有包括流感病毒、细胞、细胞因子、抗原及抗体的实时曲线图用来反映它们的数量特性。

4.1.2定义对象

为了实现系统的动画效果，我们在此定义Moveable 接口，Actor2D为一实体类，所有细胞类、细胞因子类、抗原类及抗体类都是由Actor2D派生而来。

4.1.3系统的流程描述

系统首先进入初始化，然后进行参数设置，最后启动动画模拟程序。

4.1.4系统接口

接口名：Moveable

功能描述:可移动的对象必须实现该接口

方法描述:getBounds( ):得到边界

collidesWith( ):碰撞检测

processCollisions( ):处理碰撞

update():更新对象

4.1.5系统实体类

类名:Actor2D

功能描述:场景中的角色

构造函数:Actor2D( )

成员描述:pos:位置

vel:运动方向向量

bounds:物体的边界盒

frameWidth: 运动边界x边界宽度

frameHeight: 运动边界y边界宽度

方法描述:initial():初始化

setPos(Vector2D):设置坐标

本文为全文原貌 未安装PDF浏览器用户请先下载安装 原版全文

getPos():返回坐标

getVel():返回运动方向向量

setFrameBounds(int, int):设置运动边界

getFrameBounds():返回运动边界

getFrameWidth():返回运动边界x边界宽度

getFrameHeight():返回运动边界y边界宽度

checkBounds():将物体限定在运动边界内

updateBounds():更新物体边界盒

getBounds():返回物体边界盒

collidesWith(Moveable) :碰撞检测

update():更新对象的位置和边界盒

4.1.6动画控制类

类名:AnimationControl

功能描述:控制动画的流程

构造函数:AnimationControl( )

成员描述:animateJPanel : 动画面板

statuePanel : 状态面板

showCellNumJFrame : 细胞数量曲线图显示面板

animation : 动画线程

offscreen : 图像缓冲

frameRate : 帧速

totalSeconds : 总共耗费的时间

totalFrame : 总的帧数

g2d : 绘图句柄

方法描述:initial():初始化

getFrameRate():返回帧速

setFrameRate(int) :设置帧速

start():开始动画线程

resume():恢复动画线程

pause():暂停动画线程

stop():停止动画线程

run():线程运行的主方法

updateStatuePanel():更新状态面板

paintCellMovePanel():绘制细胞运动面板

paintCellNumPanel():绘制细胞及细胞因子数量曲线图显示面板

getOffscreen():返回图像缓冲

createOffscreen(boolean) :是否生成图像缓冲

createGraphics(boolean, boolean) :生成图像句柄

4.2系统模拟

模型采用一种交互式的界面，验证过程中图形的演示完全由用户自行控制。在开发过程中采用C++语言，用面向对象的方法来实现该模型的设计。

在仿真过程中，我们主要从时间上对其进行调控，在等时间内，每一次运行的细胞、细胞因子、抗原及抗体的数量会有所不同。同时，我们也可以以抗原的数量为基准来观察其它实体的数量变化。但由于生物学中免疫系统的免疫具有周期性的规律，所以我们主要采用第一种方式，以期能从中验证生物免疫规律或是从中发现规律，以促进对流感病毒入侵免疫系统的的研究。

5 结论

B方法是一种基于自动定理证明的成熟的形式化方法。它利用本身的优势来帮助解决在生物学或者其他领域中碰到的很多仅仅靠当前的实验条件还无法完全解决的复杂问题，对生物学领域的发展起着至关重要的意义。

参考文献：

[1]裘宗燕.译.B方法.北京:电子工业出版社,2004.

[2]邹盛荣,郑国梁.B语言和方法与Z、VDM的比较.计算机科学,2002(10):136-138.

[3]陆德源.现代免疫学.上海:上海科技出版社,1995.

[4]李涛.著.计算机免疫学.北京:电子工业出版社,2004.

注：本文中所涉及到的图表、注解、公式等内容请以PDF格式阅读原文。

本文为全文原貌 未安装PDF浏览器用户请先下载安装 原版全文