Visible to the public File preview

Assuring the Safety, Security, and Reliability of Medical-Device CPS
Insup Lee PRECISE Center Department of Computer and Information Science University of Pennsylvania

NSF CPS PI Meeting August 1, 2011

Team members
•  Penn, SEAS
–  –  –  –  –  –  Insup Lee (PI) Rajeev Alur Rahul Mangharam George Pappas Rita Powell Oleg Sokolsky William Hanson, III, MD Margaret Mullen-Fortino, RN Soojin Park, MD Victoria Rich, RN

•  • 

MGH/CIMIT
–  Julian Goldman, MD

Minnesota
–  –  –  –  Mats Heimdahl Nicholas Hopper Yongdae Kim Michael Whalen

• 

Penn, UPHS/SoM
–  –  –  – 

• 

Waterloo
–  Sebastian Fischmeister

• 

Collaborators
–  –  –  –  John Hatcliff, KSU Paul Jones, FDA Sandy Weininger, FDA Zhang Yi, FDA

• 

Penn, Sociology, SAS
–  Ross Koppel

CPS: Large: Assuring the Safety, Security and Reliability of Medical Device Cyber Physical Systems (NSF CNS-1035715) Affiliated Project:
•  Medical Device NIH/NIBIB Quantum Grant: Development of a Prototype Healthcare Intranet for Improved Health Outcomes (PI: Julian Goldman)

Trends in MCPS (Medical CPS)
Autonomy • Physiological closed loop control • Context-sensitive decision support • Smart alarms Teleoperation • Robotic surgery • Tele-ICU

Miniaturization Interoperation • Implantable devices • Executable clinical • Ingestible sensors scenarios • Safety interlocks

MCPS Research Challenges (partial list)
•  High-confidence medical software systems •  Medical device integration and interoperation •  Patient modeling and simulation •  Adaptive patient-specific algorithms •  User-centered design and caregiver modeling •  Incremental and compositional methods for certifiable assurance and safety

Our MDCPS Research
•  High-confidence medical software systems
–  Evidence-based development –  GPCA (Generic Patient-Controlled Analgesia) infusion pump –  Pacemaker challenge problem

•  Medical device interoperability platform
–  VMD (virtual medical device) –  Security and Privacy

•  Smart alarms & decision support •  Physiological closed-the-loop •  Assurance and Certification

Infusion Pump Safety
•  During 2005 and 2009, FDA received approximately 56,000 reports of adverse events associated with the use of infusion pumps
•  1% deaths, 34% serious injuries •  87 infusion pump recalls to address safety problems

•  The most common types of problems
–  Software Defect –  User Interface Issues –  Mechanical or Electrical Failure
U.S. Food and Drug Administration, Center for Devices and Radiological Health. White Paper: Infusion Pump Improvement Initiative, April 2010

GPCA reference implementation
•  FDA initiated
–  GPCA Safety Requirements –  GPCA Model (Simulink/Stateflow)
Safety Requirements GPCA Model

•  Develop a GPCA reference implementation •  Provide evidence that the implementation satisfies the safety requirements
–  Safety cases –  Confidence cases

Formal Modeling & Verification Automated Implementation

Testing

•  All artifacts to be available as open source
–  http://rtg.cis.upenn.edu/gip.php3

GPCA Reference Implementation

Model-Based Development of GPCA Reference Implementation

Model-based GPCA Implementation
GPCA Safety Requirements Test sequences GPCA Model (Simulink/Stateflow) Test sequences

Manual translation

Manual translation External Channels Clock Source

UPPAAL Queries

UPPAAL Model

Formal Verification

Code-Synthesis (TIMES tool)

Manual Implementation

Verification Result (Yes/No)

Platform-Independent Code (C code)

Glue-Code

Model Trace

Code-Interfacing Compilation

Validation Result

Validation

Implementation Trace

Executable Image of the target platform

[Kim et al, EMSOFT 2011]

Medel-based development of pacemaker
Model-Driven Development + Timing Analysis
Software life cycle Requirement analysis (1) Design Implementation Integration

Development process

System spec. (2)

Timed automata model of pacemaker

(3) synthesis C code compiled into

Verification and validation process

Model checking with UPPAAL (5) Rechecking with ∆

(4) Measurement based timing analysis
Manual Semi-automatic Automatic

Heart Modeling

[Mangharam]

Network enabled devices…
Many modern medical devices are network-enabled...
RxStation / Ethernet Anesthesia Machine Ethernet

Ethernet / 802.11b

RS-232 to Ethernet Adapter

Are we fully leveraging this connectivity?

Portable Monitor 802.11b

ECG Cart Ethernet

Interoperability and Compositionality
Characteris*cs •  Medical
 devices
 gaining
  communica1on
 capabili1es
 
  •  Devices
 s1ll
 operate
 independently
  •  Standardized
 interac1on
 between
  devices
 non
 existent
  •  Full
 benefit
 of
 communica1on
  capabili1es
 not
 being
 realized
 
Advantages

Current
  Future
 

MD
 PnP:
 Interoperable
 medical
 devices
 based
 on
  plug-­‐n-­‐play!
  Vendor
 neutrality
 based
 on
 virtualiza1on
 (virtual
  medical
 device
 interfaces)

• Improve
 Pa1ent
 safety
  • Complete,
 accurate
 medical
  records
  • Reduce
 errors
  • Context
 awareness
  • Rapid
 deployment
  • Safety
 interlocks
 

Virtual Medical Devices (VMD)
•  MD PnP (initiative for medical devices interoperability) enables a new kind of medical device, a Virtual Medical Device (VMD). •  VMD is a set of medical devices coordinating over a network for clinical scenario. •  VMD does not physically exist until instantiated at a hospital. •  The Medical Device Coordination Framework (MDCF) is prototype middleware for managing the correct composition of medical devices into VMD.

+
Device Coordination Algorithm Medical Device Types

=
Virtual Medical Device (VMD)

MDCF
•  •  Clinician selects appropriate VMD MDCF binds appropriate devices into VMD instance MDCF displays VMD GUI for clinician

VMD Research Issues
•  Real-time support for VMD Apps
–  Real-time communication infrastructure –  Pub/sub programming model –  Support for programming clinicalalgorithms with real-time constraints –  Event driven & Time triggered –  Guarantee performance specified by VMD App or prevent clinician from instantiating VMD

VMD App Validation & Verification

• 

MDCF Platform
–  –  –  – 

Device connection protocols Device configuration protocols VMD setup/tear-down algorithm Export specification to Verify that platform: model-checker for verification •  Correctly implements protocols •  Instantiation of VMD is safe Co-Developed with •  Runtime verification

Generate simulation models directly from executable VMD App specification (for validation)

NSF CNS-0930647 (PI: John Hatcliff) Medical Device NIH/NIBIB Quantum Grant (PI: Julian Goldman)

Smart Alarm and Decision Support
•  VMD of multiple devices and central “smart” controller
–  Filter, combine, process, and present real-time medical information –  Suppress clinically irrelevant alarms –  Provide summaries of the patient's state and predictions of future trends

•  Benefits
–  Improves patient safety –  Reduces clinician workload –  Facilitates practice of evidence-based medicine

•  Challenges
–  Filtering and combining data streams from multiple devices (clock synch?) –  Developing context-aware patient models –  Encoding hospital guidelines, extracting experts' models, learning models statistically –  Presenting data concisely and effectively

Generic Smart Alarm
•  Generic Smart Alarm Architecture —  Modular: flexible and configurable —  Preprocessing, inference, visualization —  3-pronged approach •  Case Study
— 

Smart alarm for CABG patients
•  • 

Post-CABG surgery patients produce many false alarms Simple classification with nurse-generated rules: 57% reduction in false alarms

—  — 

Seizure smart alarm Vasospasm smart alarm

• 

Issues
–  – 

Simplify design to ease workflow integration Understand and establish safety in these systems

Networked Physiological Closed-Loop Systems
•  Benefits
–  Improved patient safety –  Improved clinical outcomes –  Reduced deployment cost
•  Networking existing medical devices

•  Clinical Use Cases
–  Closed-loop PCA –  Closed-loop Blood Glucose (BG) Control –  Ventilator weaning procedure

•  Challenges
–  Hazard identification and mitigation
•  Network packet delay/drop, sensor disconnection, out-of-sync between controller and devices Hybrid (continuous physiology + discrete controller) system simulation & formal verification

–  System modeling and analysis
• 

Certification
•  In the U.S., FDA approves medical devices for specific use
–  Safety and effectiveness are assessed –  Evaluation is process-based: ISO 9001 (quality management) and ISO 14971 (risk management) –  FDA’s 510(k) requires “substantially equivalent” to devices on the market

•  Process standards are just one part of the picture
–  Evidence about the product should play a larger role, which provides a reasonable assurance of safety and effectiveness

•  Certification of interoperable MCPS
–  Currently, each collection of interconnected devices is a new medical device to be approved. Unsustainable! –  Can we approve virtual medical devices or clinical scenarios?

Assurance and Certification
•  In search of an evidence-based regulatory regime
–  Suggested by: Software for Dependable Systems: Sufficient Evidence? D. Jackson, M. Thomas, and L.I. Millett, Eds., National Academies Press, 2007 –  Assurance cases have been suggested as the basis for evidence-based certification
•  Means of organizing argument •  Goal-Structured Notation

Context

Goal Strategy Sub-Goal Sub-Goal

–  Assurance cases
•  Safety cases •  Confidence cases •  Security cases

Evidence

Evidence

–  Industry day on assurance cases for medical devices, U. Minnesota, July 28, 2011 •  Incremental and compositional assurance and certification

THANK
 YOU!
 

http://precise.seas.upenn.edu