Citation
Rahul Mangharam. "Closing the loop with Medical Cyber-Physical Modeling". Talk or presentation, 2, November, 2012.

Abstract
The design of bug-free and safe medical device software is challenging, especially in complex implantable devices that control and actuate organs whose response is not fully understood. Safety recalls of pacemakers and implantable cardioverter defibrillators between 1990 and 2000 affected over 600,000 devices. Of these, 200,000 or 41%, were due to firmware issues (i.e. software) that continue to increase in frequency. There is currently no formal methodology or open experimental platform to test and verify the correct operation of medical device software within the closed-loop context of the patient. IN this talk I will describe our efforts to develop the foundations of modeling, synthesis and development of verified medical device software and systems from verified closed-loop models of the device and organs. The research spans both implantable medical devices such as cardiac pacemakers and physiological control systems such as drug infusion pumps which have multiple networked medical systems. In both cases, the devices are physically connected to the body and exert direct control over the physiology and safety of the patient. With the goal to develop a tool-chain for certifiable software for medical devices, I will walk through (a) formal modeling of the heart and pacemaker in timed automata, (b) verification of the closed-loop system, (c) automatic model translation from UPPAAL to Stateflow for simulation-based testing, and (d) automatic code generation for platform-level testing of the heart and real pacemakers. If time permits, I will describe our investigations in distributed wireless control networks and green scheduling for energy-efficient building automation.

Electronic downloads

• dreams-mangharam-2012.pdf · application/download · 17748 kbytes

• HTML

  Rahul Mangharam. <a
  href="http://chess.eecs.berkeley.edu/pubs/947.html"
  ><i>Closing the loop with Medical Cyber-Physical
  Modeling</i></a>, Talk or presentation,  2,
  November, 2012.

• Plain text

  Rahul Mangharam. "Closing the loop with Medical
  Cyber-Physical Modeling". Talk or presentation,  2,
  November, 2012.

• BibTeX

  @presentation{Mangharam12_ClosingLoopWithMedicalCyberPhysicalModeling,
      author = {Rahul Mangharam},
      title = {Closing the loop with Medical Cyber-Physical
                Modeling},
      day = {2},
      month = {November},
      year = {2012},
      abstract = {The design of bug-free and safe medical device
                software is challenging, especially in complex
                implantable devices that control and actuate
                organs whose response is not fully understood.
                Safety recalls of pacemakers and implantable
                cardioverter defibrillators between 1990 and 2000
                affected over 600,000 devices. Of these, 200,000
                or 41%, were due to firmware issues (i.e.
                software) that continue to increase in frequency.
                There is currently no formal methodology or open
                experimental platform to test and verify the
                correct operation of medical device software
                within the closed-loop context of the patient. IN
                this talk I will describe our efforts to develop
                the foundations of modeling, synthesis and
                development of verified medical device software
                and systems from verified closed-loop models of
                the device and organs. The research spans both
                implantable medical devices such as cardiac
                pacemakers and physiological control systems such
                as drug infusion pumps which have multiple
                networked medical systems. In both cases, the
                devices are physically connected to the body and
                exert direct control over the physiology and
                safety of the patient. With the goal to develop a
                tool-chain for certifiable software for medical
                devices, I will walk through (a) formal modeling
                of the heart and pacemaker in timed automata, (b)
                verification of the closed-loop system, (c)
                automatic model translation from UPPAAL to
                Stateflow for simulation-based testing, and (d)
                automatic code generation for platform-level
                testing of the heart and real pacemakers. If time
                permits, I will describe our investigations in
                distributed wireless control networks and green
                scheduling for energy-efficient building
                automation. },
      URL = {http://chess.eecs.berkeley.edu/pubs/947.html}
  }
  

Posted by David Broman on 7 Nov 2012.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.