Formal Specifications and Analysis of the Computer Assisted Resuscitation Algorithm (CARA) Infusion Pump Control System

基于计算机辅助复苏算法（CARA）注射泵控制系统的形式规范和分析

摘要：为了学习需求捕获方法的应用和分析输液泵控制系统，我们将整个方法分为两步。第一步，将不规范的设计需求变换为一套参考规范，该规范利用了以EFSM （Extended Finite State Machines 有限状态扩展机构）的形式的正规系统。第二步，将这些参考规范翻译成支持形式分析的工具，比如SCR,CHARON和Hermes，将有利于我们判断参考规范的性质。我们的研究目的是为集成应用正式方法，研究发展一种框架和方法论，该方法将用于一些高可靠性的医疗系统中。

1、概述

       本文基于Walter Reed军事研究所研制的输液泵系统进行研究。

       SCR能够帮助我们进行覆盖检查(coverage checks), CHARON将帮助我们进行混合系统的模拟，该混合系统包括离散和连续的行动，Hermes将帮助我们检查安全属性。

2.CARA概述

CARA是一个可以决定注射速度的系统，比如在人在失血过多、需要注射生理盐水的情况下。CARA通过病人的血压来决定注射速度的快慢，它包括一个注射泵和一个生理监测设备。生理数据包括无创袖带检测的血压，脉搏速度和动脉压。CARA包括一个含有M100的输液泵和一个生理状态监测设备。生理状态监测设备监测的生理参数主要包括无创袖带血压，脉搏速度或者是静脉血压。整个系统由一下部分组成：CARA算法、泵、血压传感器、医生、和病人。

       CARA：CARA将会驱动输液泵将病人血压升高，并维持在一个适当的范围。根据病人当前血压和医生设定的平均血压，CARA算法可以计算出理想的输液速度。理想的平均血压的设定值为70mmHg。

       CARA通过显示屏可以显示报警信号、病人信息，输入设备为软键盘。当输液泵出现错误时，将激活报警信号。

       泵：输液泵有两种模式，手动模式和自动控制模式。在手动模式下，输液速度可以有泵内部的开关设定。在自动控制模式下，输液泵的输液速度由外部电压的自控电压控制。

    医护人员：医护人员通过屏幕上的软键盘可以将血压值设定在一个适当的范围，

3.基于EFSM的CARA的参考仿真规范

       正如前述所讲，第一步要敬爱那个非正规的要求转换成正式的参考规范。WRAIR研究所提供了一个要求列表和问答列表。我们将其利用21个EFSM系统（扩展有限状态机构系统）归纳为一个CARA系统。一个EFSM是一个带有变量的有限状态机构。在我们的模型下，这些状态有限机构利用共有变量进行通信。以这种方式归纳该系统的目的在于，能够使我们建立一个标准的文档，工作组的每一位成员可以参考该文档。我们创建EFSM的目的在于以一种精确的严格的方法归纳可以我们理解的要求文档。然后利用各种分析技术将EFSMs转换成另一种形式。

3.1.CARA的整体结构

       包括医护界面、血压监测、算法和泵监测。算法部分的目的是根据采样数据控制输液泵的注射速度。根据病人的血压可以计算出泵的注射速度，血压越高速度越慢。监护界面有两个功能。第一，可以作为和医护人员交流的通道，医护人员可以通过界面预设目标血压，启动和停止输液泵。第二，它能够显示错误信息，产生报警声音。错误信息有二，泵的故障和病人/输液错误。

       BP监测仪根据多种信号源设计，比如静脉压、脉搏速度、袖带传感器，在计算之后，将会选择最好的信号源。同时，将会计算病人的血压变换，以发出报警。

       泵监测仪主要监测泵是否工作正常，检查是否堵塞、输出是否正常。包括堵塞监测、阻抗监测、注射速度监测。

3.2、基于EFSM技术的CARA算法仿真

       CARA的四个内部元器件的分层结构如图4。

l        泵监测器主要由六个EFSM’s进行仿真。监测堵塞、监测气道通畅、监测OccOK，监测连续性，通过这几个监测，判断输入信号是否可用，控制输液容积和速度；

l        BP监测器主要有三个EFSM组成

l        监测界面

l        算法用来选择当前的CARA模式，并且执行Polling算法。根据泵的当前状态从一种模式切换到另一中模式。根据血压值，控制泵的流速。

3.3 细节举例

       主要详细介绍了EFSM的创建过程，EFSM根据需求创建，在使得不同机构通信简便化方面有着重要意义。

3.4.将EFSM作为规范

       主要介绍了利用EFSM方法作为规范后的意义。

4.基于SCR工具的CARA

       SCR（Software Cost Reduction）是一个正规的形式规范方法。工程师可以利用这个方法对这个系统进行一些详细的说明要求和规定。SCR由详细的编译器、仿真器和一套分析工具组成。规范编辑器将系统信息输入表格中，还有一些可视化的设计工具。

SCR图表

5.基于Hermes的CARA工具

       Hermes是一个模形检验器，操作层次模块。Hermes输入语言是基于层次化的反应模块。利用Hermes，我们能够将EFSM模型具体化。

5.1建模

       我们的Hermes模型由30个模块组成。

5.2分析

       Hermes有两个模型机理描述系统需求。

6.相关工作

      我们描述了其他已经做了的工作，这些工作都是利用有限状态机构（EFSM）技术。利用这些模型，我们证明了这些系统的属性，同时我们讨论了这些工作和我们工作的不同。

7.结论

       我们利用了形式方法工具描述我们正在做的工程，基于输液泵系统分析了CARA技术。我们初步的工作是基于SCR和Hermes的。如同文中提到的，我们在提供给我们的信息要求中发现了一些错误和不完善的地方。目前的工作是鉴别其安全属性。该安全属性是由CARA建立，并由Hermes经过验证的。
       理想而言，这种形式分析方法和分析技术将会应用与高可靠性的医疗系统中。

*博客内容为网友个人发布，仅代表博主个人观点，如有侵权请联系工作人员删除。