Robotics Seminar Series: "Closing the loop with Cyber-Physical System Modeling"
Friday, February 22, 2013
3:00 PM-4:30 PM
Cyber-Physical Systems are the next generation of embedded systems with the tight integration of computing, communication and control of "messy" plants. I will describe our recent efforts in modeling for scheduling and control of closed-loop Cyber-Physical Systems across the domains of medical devices, energy-efficient buildings and programmable automotive systems.
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. 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 pacemaker and the heart.
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. More details here. As time permits, I will describe our investigations in energy-efficient building automation in which we coordinate scheduling of controllers for peak power minimization across multiple plants.
We will also briefly discuss in-vehicle and networked vehicle-to- vehicle programmable automotive architectures for the future.