The CARA simulation applet we have developed is not intended to be simply an ad hoc implementation of a CARA prototype. Rather, it is my intention that this model serve as a reference version to be used as a basis for formal verification attempts. Below we describe why I felt that such a model is necessary, why I chose Java for the modeling language, and what restrictions I imposed on the coding of the model in Java.
We are interested in the application of formal verification techniques such as model checking to the development of safety-critical embedded systems, of which CARA is a good example. The CARA system is sufficiently complex as to provide a challenge to current formal verification techniques, but sufficiently simple that it is reasonable to set as a goal the verification of important properties that encompass most or all of the system. That is, CARA can serve as a good driving example for our research in formal verification.
In order to apply formal verification techniques to CARA, it is necessary to have a formal model to verify. In late January 2001 we were provided by Walter Reed Army Institute of Research (WRAIR) some requirements documents they had developed for CARA. Some of these documents consisted of stylized lists of numbered items detailing various behavioral requirements on the CARA system. Another document consisted of informal English prose giving an overview of the system and its intended mode of use. Since a completed CARA system did not exist at that time, it was necessary for us to accept these requirements documents as the authoritative description of CARA.
From February, 2001 to early June, 2001, two members of our group (Prof. Arne Skou from Aalborg University in Denmark who was visiting Stony Brook during the period, and Stony Brook Ph.D. student Arnab Ray) worked on formalizing portions of the CARA requirements using the UPPAAL and Concurrency Workbench verification tools. Another document describes the status of that work as of June, 2001. However, certain limitations of that work were apparent to me at that time. Specifically, in the process of trying to construct formal models of the CARA system in the rather low-level languages provided by the formal verification tools, quite a number of abstractions and simplifications had been made, with the result that it seemed very difficult to make a strong case that the formalizations faithfully captured "the CARA system", or that properties formally verified about the model had any implications for the real system.
To develop a more comprehensive model of CARA that fully and faithfully captured the content of the requirements documents, it seemed necessary to me that the model be coded in a higher-level language than that provided by the verification tools we were using. In addition, it seemed necessary to have computerized support for checking the consistency of the model in various ways; for example, to make sure that all the services required by the various modules in the system were actually implemented somewhere. Finally, I felt that it would be very difficult to remove from the model the large number of obvious errors that were bound to be present, without having some capability of executing or simulating the model to permit the use of traditional debugging techniques. Only once the model had been cleared of the most blatant errors would it make sense to look for the kind of subtle problems for which formal verification would be most useful.
To address the issues laid out above, I decided that it would be useful to develop a formalization of the CARA requirements using the Java programming language. By coding the model in Java, the Java compiler could be used to perform various consistency checks. Since Java is a full-fledged programming language, it would be possible to execute the model and eliminate major errors using traditional debugging. Finally Java also comes with the Javadoc documentation generator, which generates browsable HTML documentation from specially formatted comments included with the source code. Documentation generated in this way would be a great help in keeping track of details of the model as it was developed.
It is important to note that, even though a formal model of CARA constructed in Java would be executable, I did not intend for this model to be the same thing as an implementation of the system. In general, the formal model would be more abstract than an actual implementation: we would attempt not to introduce details into the model that were neither mentioned explicitly in the requirements nor implicit from the manner in which they were stated. In particular, the formal model would avoid any platform-dependent considerations, such as whether the final system would be event-driven or interrupt driven, except insofar as seemed relevant to an accurate rendering of the requirements.
Although the use of Java to code the CARA model would free us to a great extent from distracting constraints imposed by low-level modeling languages, if arbitrary features of Java were to be used in the model it would be impossible for the model to serve as a reference for formal verification. So, I imposed a number of restrictions on the way in which the model was coded, to keep the distance from becoming too great between the Java reference model and low-level versions used for formal verification. These restrictions are detailed below. Overall, the effect of these restrictions is to ensure that the CARA model can be viewed as a large state machine that is defined as the parallel composition of a number of components. Such a view is close to that required for coding the model in a low-level process-algebraic language.
We adopted a decomposition of the CARA system into a small, fixed set of communicating modules. CARA is simple enough that an adequate modularization is obtained in this way. Each module is represented by a single Java class, whose methods correspond to services that can be invoked by other modules.
There are three basic types of modules: (1) those that represent
entities (such as the patient or the infusion pump) external
to the CARA system, (2) modules internal the CARA system,
and (3) a single special Simulation module which
we do not regard as part of the CARA model proper.
Modules representing external entities provide a run()
loop that is activated by its own concurrently executing thread.
Blocking between iterations of this loop is achieved by calls to
a delay() method of the Simulation class.
Modules internal to the CARA system do not have their own threads,
and behave in a purely reactive fashion without any loops or
blocking. Any scheduling of future events that is required
is performed by invoking methods of the Timer
module. When the scheduled time arrives, the Timer
module invokes the event by calling back to the requesting
module.
All fields and methods of the various modules are declared
static, and no dynamic instances (i.e. objects)
of any of these are created.
All fields of the classes representing system modules are
declared private or protected,
so that only methods within a class have direct access to the
fields of that class. The protected declaration
is used when the graphical user interface (GUI) requires access
to a state variable, as explained in more detail below.
Although methods of the system modules can take arguments,
the non-private methods of these classes (representing services
exported to other modules) must return void.
If a value is to be returned as the result of invoking a service,
this has to be accomplished by a callback to the invoking module.
The purpose of this restriction is to make the interaction
between modules close to the kind of message-passing discipline
typically present in the process-algebraic languages used by
formal verification tools.
In some of the modules, we use private methods that return
a return value. These are regarded as macros introduced for the
purpose of shortening or simplifying the internal code for a module.
Each non-private method provided by a system module is called by just one other module. If a module has to provide a similar service to several other modules, a separate non-private method must be exported for each other module that requires the service. Partly the purpose of this restriction is so that when a value is to be returned by callback it is unambiguous to which module the callback should go. Another purpose is to make the interaction between modules correspond to the kind of communication-by-synchronization facility typically present in process algebraic languages.
Except for the run() loops provided by modules
representing entities external to the CARA system,
the code for each method (both private and non-private) of a module
is required to be "straight-line" code that does not contain
loops or blocking. The "no-loops" restriction was violated
in a few places, but in each case the loops that were introduced
are bounded loops that can be regarded as macros that would
expand to straight-line code.
No recursive methods are allowed.
The idea underlying these restrictions is to support the following
synchronization model: once a service provided by a module is invoked
by a thread, it executes to completion without interruption
by concurrent activities initiated by some other thread.
The state variables (fields) of each module are always
simple boolean, integer, or floating point variables;
no data structures are used.
The only exception is in the AlarmControl module,
where a significant shortening of the code was achieved
by organizing the state of the many alarms into a few fixed-size
arrays that could be accessed by loops. However, except for this
shortening effect, the use of arrays and loops is inessential,
and they can be regarded as macros that expand
to straight-line code accessing simple variables.
The CARA simulation applet contains a graphical user interface (GUI) that makes it possible to control the simulation and to view important internal state variables of the various modules. It is important to note that we do not regard the GUI code as part of the formal CARA model, and in fact the GUI code has been introduced in such a way that it has very limited coupling with the formal model, and calls to the GUI do not appear at all in the formal model part of the code.
The decoupling of the GUI and the formal model was achieved in
the following way: each of the classes representing a system
module has an associated subclass that is responsible for
the GUI panel associated with that module. As a subclass, the
GUI has access to all the internal state variables of the
system module, assuming that these are declared protected
rather than private. When the simulation is initialized,
an instance of the GUI panel for each module is set, and a thread
is created and given the responsibility of updating the GUI display
periodically (once a second). When the GUI display needs to be updated,
the thread, executing in the GUI subclass, "peeks" at the current
values of the state variables and updates the display appropriately.
In this way, the GUI display is kept up-to-date without having to
make explicit calls from the formal model to the GUI.
The GUI subclass associated with the Dialog module
of the CARA system has an additional responsibility.
By peeking at the state of state variables of the Dialog
module, the GUI subclass can determine which user controls are currently
supposed to be displayed. When the user activates one of these
controls (say, clicking a button), the GUI subclass invokes
a method of the main Dialog class to indicate that
the control has been activated. This is the only situation in which
a GUI subclass invokes methods of its associated main class.
The GUI subclasses are completely separate from their associated main classes, and their code appears in separate files. It is thus possible to work on the formal model without any chance of confusion between which code constitutes the formal model and which constitutes the GUI.
BACK to Cara Infusion Pump Project.