Joint Energy Laboratories: Reliable Embedded Systems for Connected Clean Vehicles and Smart Grid
Primary Investigator (PI)
Prof. Lei He
Prof. Rupak Majumdar
Prof. Paulo Tabuada
Circuit Synthesis and Verification for Fault Tolerance
Software testing and validation
Energy storage is a key component for smart grid, renewable energy, smart building and electric vehicle (EV). For example, battery and battery management system counts for a half of the cost for an EV. Leveraging measurement based calibration, formal validation, and EV testbed, we study battery modeling and management algorithms and develop reliable software/hardware co-designed embedded systems for battery management.
We also investigate interaction between energy storage, smart building and EV fleets in the context of micro-grid with renewable energy harvest together with mobile and stationed energy storage, and develop demand response algorithms and systems for smart grid.
A Universal Battery State of Charge Model State-of-charge (SOC) measures energy left in a battery, and it is critical for modeling and managing batteries. Developing efficient yet accurate SOC algorithms remains a challenging task. Most existing work uses regression based on a time-variant circuit model, which may be hard to converge and often does not apply to different types of batteries. Knowing open-circuit voltage (OCV) leads to SOC due to the well known mapping between OCV and SOC. In this paper, we propose an efficient yet accurate OCV algorithm that applies to all types of batteries. Using linear system analysis but without a circuit model, we calculate OCV based on the sampled terminal voltage and discharge current of the battery. Experiments show that our algorithm is numerically stable, robust to history dependent error, and obtains SOC with less than 4% error compared to a detailed battery simulation for a variety of batteries. Our OCV algorithm is also efficient, and can be used as a real-time electro-analytical tool revealing what is going on inside the battery.
A DC/DC converter with zero-voltage switching One way to balance battery cells is to use DC/DC converter. We develop a power-efficient PWM DC/DC converter design with a novel zero voltage switching (ZVS) control technique. The ZVS control is realized by an inner feedback loop which is implemented by simple digital circuitry between the input and output of the power transistors and achieves real-time zero voltage switching (ZVS) for various loading and device parameters with power efficiencies over 90.0%. In addition, an outer feedback loop is used to ensure that the output precisely tracks a reference voltage level. We have also built the relationship between the output voltage ripple and the speed of the voltage comparators which has shown to introduce new low-frequency signals to the loops and cause significant output voltage ripples. Experiment results show that the output ripple could be reduced by 4x by carefully handling the generation and propagation of these low frequency signals.
Automatic verification of control system implementations Software implementations of controllers for physical subsystems form the core of many modern safety-critical systems such as aircraft flight control and automotive engine control. A fundamental property of such implementations is stability, the guarantee that the physical plant converges to a desired behavior under the actions of the controller. We present a methodology and a tool to perform automated static analysis of embedded controller code for stability of the controlled physical system. The design of controllers for physical systems provides not only the controllers but also mathematical proofs of their stability under idealized mathematical models. Unfortunately, since these models do not capture most of the implementation details, it is not always clear if the stability properties are retained by the software implementation, either because of software bugs, or because of imprecisions arising from fixed-precision arithmetic or timing. Our methodology is based on the following separation of concerns. First, we analyze the controller mathematical models to derive bounds on the implementation errors that can be tolerated while still guaranteeing stability. Second, we automatically analyze the controller software to check if the maximal implementation error is within the tolerance bound computed in the first step. We have implemented this methodology in Costan, a tool to check stability for controller implementations. Using Costan, we analyzed a set of control examples whose mathematical models are given in Simulink and whose C implementation is generated using Real-Time Workshop. Our technique combines analysis of the mathematical controller models and automated analysis of source code to guarantee stability properties.
Systematic testing for control applications Software controllers for physical processes are at the core of many safety-critical systems such as avionics, automotive engine control, and process control. Despite their importance, the design and implementation of software controllers remains an art form; dependability is generally poor, and the cost of verifying systems is prohibitive. We illustrate the potential of applying program analysis tools on problems in controller design and implementation by focusing on concolic execution, a technique for systematic testing for software. In particular, we demonstrate how a concolic execution tool can be modified to automatically analyze controller implementations and (a) produce test cases achieving a coverage goal, (b) synthesize ranges for controller variables that can be used to allocate bits in a fixed-point implementation, and (c) verify robustness of an implementation under input uncertainties. We have implemented these algorithms on top of the Splat test generation tool and have carried out preliminary experiments on control software that demonstrates feasibility of the techniques.
Parameterized verification of transactional memories We describe an automatic verification method to check whether transactional memories ensure strict serializability - a key property assumed of the transactional interface. Our main contribution is a technique for effectively verifying parameterized systems. The technique merges ideas from parameterized hardware and protocol verification - verification by invisible invariants and symmetry reduction - with ideas from software verification-template-based invariant generation and satisfiability checking for quantified formula (modulo theories). The combination enables us to precisely model and analyze unbounded systems while taming state explosion. Our technique enables automated proofs that two-phase locking (TPL), dynamic software transactional memory (DSTM), and transactional locking II (TL2) systems ensure strict serializability. The verification is challenging since the systems are unbounded in several dimensions: the number and length of concurrently executing transactions, and the size of the shared memory they access, have no finite limit. In contrast, state-of-the-art software model checking tools such as BLAST and TVLA are unable to validate either system, due to inherent expressiveness limitations or state explosion.
Software model checking We survey recent progress in software model checking.
C138. Bingjun Xiao, Yiyu Shi, Lei He, "A Universal State-of-Charge algorithm for Batteries", 47th IEEE Design Automation Conference (DAC'10) , Anaheim, CA, June 13-18, 2010.
C92. Changbo Long, Sasank Reddy, Lei He, Sudhakar Pamarti, and Tanay Karnik, "Power-Efficient Pulse Width Modulation DC/DC Converters with Zero Voltage Switching Control," International Symposium on Low Power Electronics and Design , October 2006.
Adolfo Anta, Rupak Majumdar, Indranil Saha, and Paulo Tabuada, "Automatic verification of control system implementations", Proceedings of the tenth ACM international conference on Embedded software (EMSOFT), ACM, 2010, Best paper award.
Rupak Majumdar, Indranil Saha, Zilong Wang, "Systematic testing for control applications", Proceedings of the 8th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2010.
Michael Emmi, Rupak Majumdar, Roman Manevich, "Parameterized verification of transactional memories", Proceedings of the 2010 ACM SIGPLAN conference on Programming language design and implementation (PLDI), 2010.
Ranjit Jhala and Rupak Majumdar, "Software model checking", ACM Computing Surveys, Volume 41 Issue 4, 2009.