Model-Based Embedded
Systems: Verification of a Medical Device Platform
This
project will have you apply what you learned about the verification of timed
automata to a new application. The new application is also in the medical
domain, and is described in the paper “Cross-layer design of platform for
closed-loop medical cyber-physical systems” by Asare et al., available on the
course webpage.
Part 1
1.
Read the
paper. You will present it to us as part of your deliverables. We need to understand, based on your explanation,
a.
what is the
problem addressed by this paper?
b.
Why is it
important? (i.e. how does it improves patients’ well-being, or what bad things is it trying to address and what
happens if they’re not addressed?)
c.
How does the
paper address this problem? This will take the most time in your presentation, but it is essential that
you explain the What and Why clearly first, otherwise the How won’t matter.
The
slides for the project, available on the course webpage, explained the setup of
the Open Medical Applications Platform (OMAP), including the notions of app
Manager, device Driver, and Device. In what follows, we distinguish between the
“true connection state”, which can be either Up or Down, and the status of the
connection that is kept in the Manager and the Driver. The latter is the
Manager’s (Driver’s) idea of the true connection state.
One
of the objectives of this work is to define a communication protocol between
the Manager, Driver, and Device(s). The protocol needs to satisfy requirements
of correctness, tolerance, consistency and fail-safety.
-
Correctness means that
A) if the true state of the d or m connections changes, then the Driver and Manager must eventually reflect
that change by updating the connection’s status (within some delay). And B) if
the true state of a connection has been constant for a while, then the Driver
and Manager must eventually reflect that state correctly (within some delay).
This is captured in Slides 8,9. Note that requirements A and B are not the same
thing.
-
Tolerance means that
if the true state of a connection changes too many times within one time unit, then the Manager and Driver
will only reach to the last value that it changed to. This ensures that noise
on the connection does not cause the rest of the platform to go haywire and try
to keep up. I expect this will be the hardest requirement to deal with.
-
Consistency means that
if the Manager changes a
connection’s status to X (X =
G,R,Y,or O), then the Driver must do
the same (possibly with some delay). Symmetrically, if the Device changes a
connection’s status, the Manager must eventually follow suit (within some
delay). This is captured on slides 11,12
-
Fail-safety means that
if some connection goes down when the Driver was In Use, and stays down for too long, then the Driver and
Manager must eventually transition to the Fail states within some delay(s).
This is (kind of) illustrated on slide 8.
2.
Express these requirements
in LTL.
a.
First,
ignore the “within some delays” portion of the requirements and write the LTL formulas. Feel free to
break down each requirement into multiple formulas. Start by expressing
Correctness, Consistency and Fail-Safety to practice, then do Tolerance.
b.
The
requirements impose real-time delays on transitions, e.g. “within 5sec”. Can you capture this in LTL
without any extra assumptions on sampling rate of signals? If you have to
impose some additional assumption, what is it and is it realistic?
c. Instead of
imposing an assumption on the signal sampling rate, you can also modify the model under verification. E.g. if “State A follows
State B within 5ms”, you can guard the transition between them how? And then
use the LTL formula “A \implies Eventually B”
Part 2
We
now need to create a particular candidate implementation of a communication
protocol and model-check that it satisfies the requirements. This will consist
of an insulin infusion app, a device Manager, two device Drivers, and two abstract devices: a patient state
monitor and a pump. The paper above lists these on p.7 (last paragraph before
the Conclusion). The monitor observes and reports on a patient state (like
blood glucose concentration), and the pump injects insulin into the patient,
based partially on the patient state. Thus a monitor should be associated to
one (or more) pumps, and measure the variables they need to know about.
I suggest you divide these
tasks amongst yourselves. Read through them all first.
3. See the
abstract monitor machine in “Monitor
behavior” PDF document. This models
how the monitor associates itself to a device. Implement this in UPPAAL.
4. See the
abstract pump machine in “Pump behavior” PDF document. Implement it in UPPAAL.
5. See the connection machine in “Device-driver connection behavior”
PDF. Complete this first: what is causing the transitions in the modes of the
machine? Some variables from the previous two machines? Or maybe you need to
model an environment that non-deterministically causes the connection to switch
between its two states? Or both?
6.
Implement the completed connection machine in UPPAAL.
7.
Design a device Manager and
model it in UPPAAL. Recall that “The
device manager and the platform API
provide the abstract variable-based interface to the applications.” So the
manager reads variables from the drivers and supplies these to the apps, and
reads values of actuation variables from the apps and supplies them to the
drivers (who relay them to the devices). It also queries the status of the m
and d connections. The entire functionality of the manager doesn’t need to be
modeled, only the aspects that are relevant for verifying the connection
protocol and the specifications you expressed earlier.
Part 3
8. Design the
app: functionality-wise, the app reads patient state (though the manager) and computes the amount of
insulin to infuse. However, you will not be modeling these computations.
Rather, you are only modeling those aspects of the app that are necessary for
checking the communication protocol.
In your
model, the app requests to connect to variable (i.e., patient state) or action
(i.e., access to an actuator on the actual device). Every variable and action
is associated to a device driver that provides that access through its device.
If the driver associated to a requested variable/action is not in the G[Idle]
state, the Manager must refuse that request. Otherwise, the driver (drv machine
on slide 8) transitions to G[In Use]
indicating
it is now busy, and the Manager reports back to the app that the connection
request has been accepted.
The app can
start doing something useful only when all its requested drivers have
transitioned to G[In Use] state.
9.
Design an
abstract environment and model it in UPPAAL. The job of this environment is to set the true
connection states for m and d (either Up or Down).
10.
Re-visit your LTL specs and make sure they are
expressed in terms of the variables and states that you used in your timed
automata models. Recall that the LTL formulas describe the behavior of the
communication protocol, not the app, or a particular device…etc.
11.
Simulate the
above system, call it S, in UPPAAL. S = parallel composition of above timed automata for app, manager,
drivers and environment.
12. Model-check
the LTL requirements on this system.
Part 4
Describe your models,
properties, and the model checking results, in writing.
0 comments:
Post a Comment