High-Confidence Medical Device Software and 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. In this effort, 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.



Energy-Efficient Building Automation –

here our interests are in scheduling of controllers (e.g. HVAC, boilers, chillers) for peak-power minimization as energy pricing is peak-power based. We are developing Green Scheduling algorithms for radiant systems, chillers and multi-building systems. We also focus on wireless sensing of the building facade to monitor the solar heat gain and its delayed effect on the power consumption of the HVAC systems. We have recently developed a tool, MLE+ Matlab-EnergyPlus Co-Simulation tool for integrated building modeling and controller design [MLE+ details here]. This is part of the Department of Energy $160M Energy-Efficient Building HUB.
See Energy Efficient Building project video and slides



Wireless Control-Actuator Networks for Industrial Automation –

The current generations of embedded wireless networks address sensing and monitoring only and are largely open loop. To address actuation and closed-loop control, the communication architecture, protocols and interaction between communication and computation need to be re-thought. My goal is to develop a new class of wireless control networks where the automation systems are ‘plug-n-play’ – i.e. the wireless controller can be hot-swapped and the wireless I/O lines reconnect and maintain control performance and safety. This requires that the control functionality is decoupled from the inherently unreliable wireless substrate and the control performance and stability is scalable with the number of nodes within the controller networks. More details on Embedded Virtual Machines, Wireless Control Networks and Anti-Jamming.
Wireless Control Networks – slides and video



Automotive Systems –

The automobile of the future will be programmable for network-based active safety, real-time traffic congestion prediction and remote vehicle diagnostics and updates. To realize this goal, we present three contributions toward the foundations of Automotive-CPS: (a) AutoPlug – An Open Automotive Platform for Electronic Controller Unit (ECU) testing, and verification for remote recalls management; (b) GrooveNet – a vehicle-to-vehicle network virtualization platform that enables communication between hundreds of virtual vehicles and real vehicles for active networked safety, and (c) AutoMatrix – a GPU-based vehicular traffic congestion simulator that can simulate over 16 million vehicles for real-time traffic congestion probing, prediction and fastest-path route assignment. Given these building blocks, we believe that Automotive-CPS wireless networks will make driving safer, more efficient and of course, more enjoyable.

Automotive systems – video and slides


Real-Time Algorithms for Parallel Architectures –

Most algorithms are run-to-completion and provide one answer upon completion and no answer if interrupted before completion. On the other hand, anytime algorithms have a monotonic increasing utility with the length of execution time. Our investigation focuses on the development of time-bounded anytime algorithms on Graphics Processing Units (GPUs) to trade-off the quality of output with execution time. Given a time-varying workload, the algorithm continually measures its progress and the remaining contract time to decide its execution pathway and select system resources required to maximize the quality of the result. To exploit the quality-time tradeoff, the focus is on the construction, instrumentation, on-line measurement and decision making of algorithms capable of efficiently managing GPU resources. We demonstrate this with a Parallel A* routing algorithm on a CUDA-enabled GPU. The algorithm execution time and resource usage is described in terms of CUDA kernels constructed at design-time. At runtime, the algorithm selects a subset of kernels and composes them to maximize the quality for the remaining contract time. We demonstrate the feedback-control between the GPU-CPU to achieve controllable computation tardiness by throttling request admissions and the processing precision. As a case study, we have implemented AutoMatrix, a GPU-based vehicle traffic simulator for real-time congestion management which scales up to 16 million vehicles on a US street map. This is an early effort to enable imprecise and approximate real-time computation on parallel architectures for stream-based timebounded applications such as traffic congestion prediction and route allocation for large transportation networks.

RTAlgorithms for Parallel Architectures – video and slides