|
|
|||||||||||||
|
|
|||||||||||||
|
|
Joint Energy Laboratories: Reliable Embedded Systems for Connected Clean Vehicles and Smart Grid
Prof. Lei He Min Gao NF Jing
Circuit Synthesis and Verification for Fault Tolerance
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.
|
Send
your comments to our webmaster.
Last update: 01-31-2008.