This project develops the foundations of modeling, synthesis and development of verified medical device software and systems, from verified closed-loop models of the device and organ(s). The effort spans both implantable medical devices such as cardiac pacemakers and physiological control systems such as drug infusion pumps that 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-in-the-loop. The goal is to ensure the device will never drive the patient into an unsafe state, while providing effective therapy. The contributions of are in three areas: closed-loop patient-device modeling; quantitative verification for optimized patient-specific devices; platforms for life-critical systems. Integrated modeling methodologies are developed to produce both the functional physiological signals, for clinically relevant testing with a medical device, and also generate the formal timing of device-patient interaction for formal verification. Starting with the problem of verifying the safety and correctness of medical device software, probabilistic patient models based on physiological data are then used to develop quantitative verification techniques to maintain the therapy?s efficacy on the patient and operational efficiency of the device. To facilitate participation of the CPS community, the Food and Drug Administration (FDA), physicians and manufacturers, open source libraries of device/patient models, software tools for verification and model translation and hardware platforms for testing with real medical devices are developed. The closed-loop design and verification techniques for medical device software and patients, developed here, have direct potential benefits on human health, and the quality and cost of medical care. Design of bug-free and safe medical device software is challenging, especially in complex implantable devices that control and actuate organs who's 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. If successful, this project has potential to not only increase the safety of such devices, but also to accelerate the development and certification process. The latter could reduce costs, and shorten the time to market for new devices. The project also has an extensive education and outreach component, including curriculum development in medical cyber-physical systems, involvement of undergraduate and graduate students in research, and cooperation with hospitals, makers of medical devices, and the FDA. The cross-cutting nature of the project brings together communities involving clinical physicians, electrical engineers, computer scientists and regulators of health care safety.