CARA Infusion Pump Project SUNY at Stony Brook Computer Science Department Contact: Prof. Eugene W. Stark

The following items are currently available from this page:

• CARA simulation applet we are using to develop and validate our CARA model.

• Rationale and underlying philosophy for the particular modeling approach we chose.

• A paper describing the model and the modeling approach.
  • View abstract.
  • View BibTeX entry.
  • Read report (PDF).

• Overview of our CARA model, with summary descriptions of each of the modules.

• Javadoc-generated documentation for the model. This documentation shows the various modules that make up our CARA model, together with the state variables for each module and the methods the modules use to interact with each other.

• Other documents, access to which are currently limited to Stony Brook only, and which are linked here for convenience of access by members of our group.

The CARA simulation applet consists of two parts: the formal CARA model and the GUI code. Since it is our intention to use the formal CARA model as a reference model for formal verification experiments, this part has been written in a very stylized subset of Java which we expect will be easier to transfer to various verification tools. It is our intention to construct a faithful reference model of the CARA system which covers as many aspects of the system operation as possible. The GUI code is not part of the formal model, and in fact it is completely separate and decoupled from the formal model. The GUI performs its display functions by "peeking" at the model's state variables periodically and using that information to keep the screen up-to-date.

To run the applet, click on the link above. You will need Java Plug-in for your browser in order to run the applet. If you are using Internet Explorer or Netscape Navigator and you do not have Java Plug-in, you will be offered an opportunity to download it.

Once the applet has loaded, you will be presented with a display panel. The upper portions of the panel constitute the "Caregiver Console", and are intended to be a rendition of the information the real CARA system would display to the medical caregiver. The bottom portion of the panel is labeled "Simulation Internals". The various tabs on this panel give you the opportunity to view various state variable of the modules in the simulation and to influence the progress of the simulation to some extent.

The applet starts with the simulation in the paused mode. To run the simulation, click on the "Pause" button under the "Simulation Control" tab. The simulation can be run faster than real time by entering a value less than 1 into the "Time Scale" field. The "CARA Log" tab is intended to show a rendition of what would go into the actual CARA system log. The "Trace" tab is a much more detailed log of simulation internal events which is used for debugging and validating the model.

To make the simulation interesting, the modules that simulate external devices ("Pump", "Cuff Source", "Arterial Source", and "Pulse Wave Source") will undergo random failures and recoveries governed by simple two-state Markov chains. You can influence the failure state by clicking on some of the indicators on these tabs. For example, under the "Pump" tab, you can click on the "CONT", "OCC", and "Air OK" indicators to force a failure or recovery.