Kerstin Eder

University of Bristol

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Trends

Author Order

Document Type

Co-Authors

Kyriakos Georgiou

University of Bristol

Dejanira Araiza-Illan

Johnson & Johnson (Singapore)

Tony Pipe

University of the West of England

Steve Kerrison

James Cook University Singapore

Greg Chance

University of Bristol

Samuel Xavier‐de‐Souza

Universidade Federal do Rio Grande do Norte

Kris Nikov

University of Bristol

Abanoub Ghobrial

University of Bristol

Jeremy Morse

University of Bristol

Jose Nunez‐Yanez

Linköping University

Cooperative Institutions

University of Bristol

Bristol Robotics Laboratory

University of the West of England

University of York

University of Oxford

Roskilde University

IMDEA Software

Technical University of Munich

Lancaster University

University College London

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Field

On the Limitations of Analyzing Worst-Case Dynamic Energy of Processing

ACM Transactions on Embedded Computing Systems (2018)

Jeremy Morse Steve Kerrison Kerstin Eder

This paper examines dynamic energy consumption caused by data during software execution on deeply embedded microprocessors, which can be significant on some devices. In worst-case energy consumption analysis, energy models are used to find the most costly execution path. Taking each instruction's worst case energy produces a safe but overly pessimistic upper bound. Algorithms for safe and tight bounds would be desirable. We show that finding exact worst-case energy is NP-hard, and that tight bounds cannot be approximated with guaranteed safety. We conclude that any energy model targeting tightness must either sacrifice safety or accept overapproximation proportional to data-dependent energy.

10.1145/3173042

Cite

Citations (13)

RAC 2016 - Resource Aware Computing, Eindhoven, 2 April 2016

M.C.J.D. van Eekelen Kerstin Eder

Source

Cite

Citations (0)

Marimba: A Tool for Verifying Properties of Hidden Markov Models

Lecture notes in computer science (2015)

Noé Hernández Kerstin Eder Evgeni Magid Jesús Savage David A. Rosenblueth

Haskell

10.1007/978-3-319-24953-7_14

Cite

Citations (2)

Towards Automating Simulation-Based Design Verification Using ILP

Lecture notes in computer science (2007)

Kerstin Eder Peter Flach Hsiou-Wen Hsueh

Inductive logic programming

10.1007/978-3-540-73847-3_20

Cite

Citations (20)

Using Models at Runtime to Address Assurance for Self-Adaptive Systems.

Betty H. C. Cheng Kerstin Eder Martin Gogolla Lars Grunske Marin Litoiu

A self-adaptive software system modifies its behavior at runtime in response to changes within the system or in its execution environment. The ful- fillment of the system requirements needs to be guaranteed even in the presence of adverse conditions and adaptations. Thus, a key challenge for self-adaptive software systems is assurance. Traditionally, confidence in the correctness of a system is gained through a variety of activities and processes performed at de- velopment time, such as design analysis and testing. In the presence of self- adaptation, however, some of the assurance tasks may need to be performed at runtime. This need calls for the development of techniques that enable contin- uous assurance throughout the software life cycle. Fundamental to the develop- ment of runtime assurance techniques is research into the use of models at runtime

Adaptive system

Cite

Citations (3)

Energy-Optimal Configurations for Single-Node HPC Applications

arXiv (Cornell University) (2018)

Vitor R. G. Silva Alex F. A. Furtunato Kyriakos Georgiou Kerstin Eder Samuel Xavier‐de‐Souza

Energy efficiency is a growing concern for modern computing, especially for HPC due to operational costs and the environmental impact. We propose a methodology to find energy-optimal frequency and number of active cores to run single-node HPC applications using an application-agnostic power model of the architecture and an architecture-aware performance model of the application. We characterize the application performance using Support Vector Regression. The power consumption is estimated by modeling CMOS dynamic and static power without knowledge of the application. The energy-optimal configuration is estimated by minimizing the product of the power model and the performance model's outcomes. Results for four PARSEC applications with five different inputs show that the proposed approach used about 14X less energy when compared to the worst case of the default Linux DVFS governor. For the best case of the DVFS scheme, 23% savings were observed, with an overall average of 6% less energy.

10.48550/arxiv.1805.00998

Cite

Citations (0)

CyRes -- Avoiding Catastrophic Failure in Connected and Autonomous Vehicles (Extended Abstract)

arXiv (Cornell University) (2020)

Carsten Maple Peter Davies Kerstin Eder Chris Hankin Greg Chance

Existing approaches to cyber security and regulation in the automotive sector cannot achieve the quality of outcome necessary to ensure the safe mass deployment of advanced vehicle technologies and smart mobility systems. Without sustainable resilience hard-fought public trust will evaporate, derailing emerging global initiatives to improve the efficiency, safety and environmental impact of future transport. This paper introduces an operational cyber resilience methodology, CyRes, that is suitable for standardisation. The CyRes methodology itself is capable of being tested in court or by publicly appointed regulators. It is designed so that operators understand what evidence should be produced by it and are able to measure the quality of that evidence. The evidence produced is capable of being tested in court or by publicly appointed regulators. Thus, the real-world system to which the CyRes methodology has been applied is capable of operating at all times and in all places with a legally and socially acceptable value of negative consequence.

Resilience

10.48550/arxiv.2006.14890

Cite

Citations (0)

Energy Transparency for Deeply Embedded Programs

ACM Transactions on Architecture and Code Optimization (2017)

Kyriakos Georgiou Steve Kerrison Zbigniew Chamski Kerstin Eder

Energy transparency is a concept that makes a program’s energy consumption visible, from hardware up to software, through the different system layers. Such transparency can enable energy optimizations at each layer and between layers, as well as help both programmers and operating systems make energy-aware decisions. In this article, we focus on deeply embedded devices, typically used for Internet of Things (IoT) applications, and demonstrate how to enable energy transparency through existing static resource analysis (SRA) techniques and a new target-agnostic profiling technique, without hardware energy measurements. Our novel mapping technique enables software energy consumption estimations at a higher level than the Instruction Set Architecture (ISA), namely the LLVM intermediate representation (IR) level, and therefore introduces energy transparency directly to the LLVM optimizer. We apply our energy estimation techniques to a comprehensive set of benchmarks, including single- and multithreaded embedded programs from two commonly used concurrency patterns: task farms and pipelines. Using SRA, our LLVM IR results demonstrate a high accuracy with a deviation in the range of 1% from the ISA SRA. Our profiling technique captures the actual energy consumption at the LLVM IR level with an average error of 3%.

Profiling (computer programming)

Embedded software

10.1145/3046679

Cite

Citations (26)

Optimizing the flash-RAM energy trade-off in deeply embedded systems

James Pallister Kerstin Eder Simon Hollis

Deeply embedded systems often have the tightest constraints on energy consumption, requiring that they consume tiny amounts of current and run on batteries for years. However, they typically execute code directly from flash, instead of the more energy efficient RAM. We implement a novel compiler optimization ¹ that exploits the relative efficiency of RAM by statically moving carefully selected basic blocks from flash to RAM. Our technique uses integer linear programming, with an energy cost model to select a good set of basic blocks to place into RAM, without impacting stack or data storage. We evaluate our optimization on a common ARM microcontroller and succeed in reducing the average power consumption by up to 41% and reducing energy consumption by up to 22%, while increasing execution time. A case study is presented, where an application executes code then sleeps for a period of time. For this example we show that our optimization could allow the application to run on battery for up to 32% longer. We also show that for this scenario the total application energy can be reduced, even if the optimization increases the execution time of the code.

Code (set theory)

Flash Memory

10.1109/cgo.2015.7054192

Cite

Citations (5)

Verification of control systems implemented in simulink with assertion checks and theorem proving: A case study

2022 European Control Conference (ECC) (2015)

Dejanira Araiza-Illan Kerstin Eder Arthur Richards

This paper presents the verification of control systems implemented in Simulink. The goal is to ensure that high-level requirements on control performance, like stability, are satisfied by the Simulink diagram. A two stage process is proposed. First, the high-level requirements are decomposed into specific parametrized sub-requirements and implemented as assertions in Simulink. Second, the verification takes place. On one hand, the sub-requirements are verified through assertion checks in simulation. On the other hand, according to their scope, some of the sub-requirements are verified through assertion checks in simulation, and others via automatic theorem proving over an ideal mathematical model of the diagram. We compare performing only assertion checks against the use of theorem proving, to highlight the advantages of the latter. Theorem proving performs verification by computing a mathematical proof symbolically, covering the entire state space of the variables. An automatic translation tool from Simulink to the language of the theorem proving tool Why3 is also presented. The paper demonstrates our approach by verifying the stability of a simple discrete linear system.

Assertion

Scope (computer science)

10.1109/ecc.2015.7330941

Cite

Citations (15)