| Pacemaker Challenge |
|
One of the major research avenues in this project targets pacemakers, a
life-critical implantable device. Starting from the informal requirements
for a pacemaker, provided by the vendor Boston Scientific, we are undertaking
a model-driven development effort that will result in a working prototype
of the pacemaker, supplemented by an assurance case that provides evidence
that the developed prototype is safe. To date, we have developed a model of
the digital controller of the pacemaker that supports all operational modes
specified in the requirements, providing complete traceability from the
requirements to the model elements. That is, for each model element such as
a state transition, we identified a paragraph in the requirements document
that justifies the model element. This mapping from requirements to the
model forms an important part of the assurance case. We then proved, using
the state-of-the-art verification tool UPPAAL, that the controller model
satisfies some of the high-level properties listed in the requirements
document, as well as other critical properties that were identified through
the dialogue with Brian Larson, a developer at Boston Scientific. On-going efforts target generation of executable code for a particular embedded microprocessor and extending the assurance case to cover the generated code.
|
