Powertrain optimisation in a hybrid electric bus

This paper describes the use of a formal optimisation procedure to optimise a plug-in hybrid electric bus using two different case studies to meet two different performance criteria; minimum journey cost and maximum battery life. The approach is to choose a commercially available vehicle and seek to improve its performance by varying key design parameters. Central to this approach is the ability to develop a representative backward facing model of the vehicle in MATLAB/Simulink along with appropriate optimisation objective and penalty functions. The penalty functions being the margin by which a particular design fails to meet the performance specification. The model is validated against data collected from an actual vehicle and is used to estimate the vehicle performance parameters in a model-in-the-loop process within an optimisation routine. For the purposes of this paper, the journey cost/battery life over a drive cycle is optimised whilst other performance indices are met (or exceeded). Among the available optimisation methods, Powell's method and Simulated Annealing are adopted. The results show this method as a valid alternative modelling approach to vehicle powertrain optimisation. © 2012 IEEE.

Polynomial function intervals for floating-point software verification

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs. © 2014 Springer International Publishing Switzerland.