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
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