Source author record

Kerstin Eder

Kerstin Eder appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

31works
16topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

31 published item(s)

preprint2023arXiv

On Self-Supervised Dynamic Incremental Regularised Adaptation

In this paper, we give an overview of a recently developed method for dynamic domain adaptation, named DIRA, which relies on a few samples in addition to a regularisation approach, named elastic weight consolidation, to achieve state-of-the-art (SOTA) domain adaptation results. DIRA has been previously shown to perform competitively with SOTA unsupervised adaption techniques. However, a limitation of DIRA is that it relies on labels to be provided for the few samples used in adaption. This makes it a supervised technique. In this paper, we propose a modification to the DIRA method to make it self-supervised i.e. remove the need for providing labels. Our proposed approach will be evaluated experimentally in future work.

preprint2022arXiv

Integrating Formal Verification and Simulation-based Assertion Checking in a Corroborative V&V Process

Automated Vehicles (AVs) are rapidly maturing in the transportation domain. However, the complexity of the AV design problem is such that no single technique is sufficient to provide adequate validation of key properties such as safety, reliability or trustworthiness. In this vision paper, a combination of a spatial traffic logic and agent-based verification methods with a validation method that uses assertion checking of simulations is proposed. We sketch how to integrate the respective approaches within a methodological framework called Corroborative Verification and Validation (V&V).The Corroborative V&V framework identifies three different verification and validation levels for AVs (formal verification, simulation-based testing, real-world experiments) and specifies connections and evidence between these levels. We define specifications for the formal relationships that must be established between processes, system models and requirements models for the evidence from formal design verification and simulation-based testing to corroborate each other and enhance assurance confidence from verification and validation.

preprint2022arXiv

Safety Validation of Autonomous Vehicles using Assertion Checking

Safety and mission performance validation of autonomous vehicles (AVs) is a major challenge. In this paper we describe a methodology for constructing and applying assertion checks to validate the behaviour of an AV operating either in simulation or in the real world. We have identified a taxonomy of assertion types and the general format of their specification, and we have developed procedures for translating driving codes of practice to yield formal logical expressions that can be monitored automatically by computer, either by direct translation or by physical modelling. We have developed examples of assertions derived from the UK Highway Code (UKHC), as an example of a code of practice. We illustrate the approach with an example of assertion checking for vehicle overtaking, using a geospatial information system in an SQL database for validation and performance assessment. We present initial simulation and runtime monitoring experiments that apply assertions relevant in this overtaking scenario together with an analysis of the safety and mission performance characteristics measured.

preprint2021arXiv

Robust and accurate fine-grain power models for embedded systems with no on-chip PMU

This paper presents a novel approach to event-based power modelling for embedded platforms that do not have a Performance Monitoring Unit (PMU). The method involves complementing the target hardware platform, where the physical power data is measured, with another platform on which the CPU performance data, that is needed for model generation, can be collected. The methodology is used to generate accurate fine-grain power models for the the Gaisler GR712RC dual-core LEON3 fault-tolerant SPARC processor with on-board power sensors and no PMU. A Kintex UltraScale FPGA is used as the support platform to obtain the required CPU performance data, by running a soft-core representation of the dual-core LEON3 as on the GR712RC but with a PMU implementation. Both platforms execute the same benchmark set and data collection is synchronised using per-sample timestamps so that the power sensor data from the GR712RC board can be matched to the PMU data from the FPGA. The synchronised samples are then processed by the Robust Energy and Power Predictor Selection (REPPS) software in order to generate power models. The models achieve less than 2% power estimation error when validated on an industrial use-case and can successfully follow program phases, which makes them suitable for runtime power profiling.

preprint2020arXiv

An Agency-Directed Approach to Test Generation for Simulation-based Autonomous Vehicle Verification

Simulation-based verification is beneficial for assessing otherwise dangerous or costly on-road testing of autonomous vehicles (AV). This paper addresses the challenge of efficiently generating effective tests for simulation-based AV verification using software testing agents. The multi-agent system (MAS) programming paradigm offers rational agency, causality and strategic planning between multiple agents. We exploit these aspects for test generation, focusing in particular on the generation of tests that trigger the precondition of an assertion. On the example of a key assertion we show that, by encoding a variety of different behaviours respondent to the agent's perceptions of the test environment, the agency-directed approach generates twice as many effective tests than pseudo-random test generation, while being both efficient and robust. Moreover, agents can be encoded to behave naturally without compromising the effectiveness of test generation. Our results suggest that generating tests using agency-directed testing significantly improves upon random and simultaneously provides more realistic driving scenarios.

preprint2020arXiv

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

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.

preprint2020arXiv

Goal-constrained Planning Domain Model Verification of Safety Properties

The verification of planning domain models is crucial to ensure the safety, integrity and correctness of planning-based automated systems. This task is usually performed using model checking techniques. However, unconstrained application of model checkers to verify planning domain models can result in false positives, i.e.counterexamples that are unreachable by a sound planner when using the domain under verification during a planning task. In this paper, we discuss the downside of unconstrained planning domain model verification. We then introduce the notion of a valid planning counterexample, and demonstrate how model checkers, as well as state trajectory constraints planning techniques, should be used to verify planning domain models so that invalid planning counterexamples are not returned.

preprint2020arXiv

Lost in translation: Exposing hidden compiler optimization opportunities

Existing iterative compilation and machine-learning-based optimization techniques have been proven very successful in achieving better optimizations than the standard optimization levels of a compiler. However, they were not engineered to support the tuning of a compiler's optimizer as part of the compiler's daily development cycle. In this paper, we first establish the required properties which a technique must exhibit to enable such tuning. We then introduce an enhancement to the classic nightly routine testing of compilers which exhibits all the required properties, and thus, is capable of driving the improvement and tuning of the compiler's common optimizer. This is achieved by leveraging resource usage and compilation information collected while systematically exploiting prefixes of the transformations applied at standard optimization levels. Experimental evaluation using the LLVM v6.0.1 compiler demonstrated that the new approach was able to reveal hidden cross-architecture and architecture-dependent potential optimizations on two popular processors: the Intel i5-6300U and the Arm Cortex-A53-based Broadcom BCM2837 used in the Raspberry Pi 3B+. As a case study, we demonstrate how the insights from our approach enabled us to identify and remove a significant shortcoming of the CFG simplification pass of the LLVM v6.0.1 compiler.

preprint2020arXiv

Performance and Energy Trade-Offs for Parallel Applications on Heterogeneous Multi-Processing Systems

This work proposes a methodology to find performance and energy trade-offs for parallel applications running on Heterogeneous Multi-Processing systems with a single instruction-set architecture. These offer flexibility in the form of different core types and voltage and frequency pairings, defining a vast design space to explore. Therefore, for a given application, choosing a configuration that optimizes the performance and energy consumption is not straightforward. Our method proposes novel analytical models for performance and power consumption whose parameters can be fitted using only a few strategically sampled offline measurements. These models are then used to estimate an application's performance and energy consumption for the whole configuration space. In turn, these offline predictions define the choice of estimated Pareto-optimal configurations of the model, which are used to inform the selection of the configuration that the application should be executed on. The methodology was validated on an ODROID-XU3 board for eight programs from the PARSEC Benchmark, Phoronix Test Suite and Rodinia applications. The generated Pareto-optimal configuration space represented a 99% reduction of the universe of all available configurations. Energy savings of up to 59.77%, 61.38% and 17.7% were observed when compared to the performance, ondemand and powersave Linux governors, respectively, with higher or similar performance.

preprint2020arXiv

Run-Time Power Modelling in Embedded GPUs with Dynamic Voltage and Frequency Scaling

This paper investigates the application of a robust CPU-based power modelling methodology that performs an automatic search of explanatory events derived from performance counters to embedded GPUs. A 64-bit Tegra TX1 SoC is configured with DVFS enabled and multiple CUDA benchmarks are used to train and test models optimized for each frequency and voltage point. These optimized models are then compared with a simpler unified model that uses a single set of model coefficients for all frequency and voltage points of interest. To obtain this unified model, a number of experiments are conducted to extract information on idle, clock and static power to derive power usage from a single reference equation. The results show that the unified model offers competitive accuracy with an average 5\% error with four explanatory variables on the test data set and it is capable to correctly predict the impact of voltage, frequency and temperature on power consumption. This model could be used to replace direct power measurements when these are not available due to hardware limitations or worst-case analysis in emulation platforms.

preprint2020arXiv

When parallel speedups hit the memory wall

After Amdahl's trailblazing work, many other authors proposed analytical speedup models but none have considered the limiting effect of the memory wall. These models exploited aspects such as problem-size variation, memory size, communication overhead, and synchronization overhead, but data-access delays are assumed to be constant. Nevertheless, such delays can vary, for example, according to the number of cores used and the ratio between processor and memory frequencies. Given the large number of possible configurations of operating frequency and number of cores that current architectures can offer, suitable speedup models to describe such variations among these configurations are quite desirable for off-line or on-line scheduling decisions. This work proposes new parallel speedup models that account for variations of the average data-access delay to describe the limiting effect of the memory wall on parallel speedups. Analytical results indicate that the proposed modeling can capture the desired behavior while experimental hardware results validate the former. Additionally, we show that when accounting for parameters that reflect the intrinsic characteristics of the applications, such as degree of parallelism and susceptibility to the memory wall, our proposal has significant advantages over machine-learning-based modeling. Moreover, besides being black-box modeling, our experiments show that conventional machine-learning modeling needs about one order of magnitude more measurements to reach the same level of accuracy achieved in our modeling.

preprint2019arXiv

A Corroborative Approach to Verification and Validation of Human--Robot Teams

We present an approach for the verification and validation (V&V) of robot assistants in the context of human-robot interactions (HRI), to demonstrate their trustworthiness through corroborative evidence of their safety and functional correctness. Key challenges include the complex and unpredictable nature of the real world in which assistant and service robots operate, the limitations on available V&V techniques when used individually, and the consequent lack of confidence in the V&V results. Our approach, called corroborative V&V, addresses these challenges by combining several different V&V techniques; in this paper we use formal verification (model checking), simulation-based testing, and user validation in experiments with a real robot. We demonstrate our corroborative V&V approach through a handover task, the most critical part of a complex cooperative manufacturing scenario, for which we propose some safety and liveness requirements to verify and validate. We construct formal models, simulations and an experimental test rig for the HRI. To capture requirements we use temporal logic properties, assertion checkers and textual descriptions. This combination of approaches allows V&V of the HRI task at different levels of modelling detail and thoroughness of exploration, thus overcoming the individual limitations of each technique. Should the resulting V&V evidence present discrepancies, an iterative process between the different V&V techniques takes place until corroboration between the V&V techniques is gained from refining and improving the assets (i.e., system and requirement models) to represent the HRI task in a more truthful manner. Therefore, corroborative V&V affords a systematic approach to 'meta-V&V,' in which different V&V techniques can be used to corroborate and check one another, increasing the level of certainty in the results of V&V.

preprint2017arXiv

Risk-based Triggering of Bio-inspired Self-Preservation to Protect Robots from Threats

Safety in autonomous systems has been mostly studied from a human-centered perspective. Besides the loads they may carry, autonomous systems are also valuable property, and self-preservation mechanisms are needed to protect them in the presence of external threats, including malicious robots and antagonistic humans. We present a biologically inspired risk-based triggering mechanism to initiate self-preservation strategies. This mechanism considers environmental and internal system factors to measure the overall risk at any moment in time, to decide whether behaviours such as fleeing or hiding are necessary, or whether the system should continue on its task. We integrated our risk-based triggering mechanism into a delivery rover that is being attacked by a drone and evaluated its effectiveness through systematic testing in a simulated environment in Robot Operating System (ROS) and Gazebo, with a variety of different randomly generated conditions. We compared the use of the triggering mechanism and different configurations of self-preservation behaviours to not having any of these. Our results show that triggering self-preservation increases the distance between the drone and the rover for many of these configurations, and, in some instances, the drone does not catch up with the rover. Our study demonstrates the benefits of embedding risk awareness and self-preservation into autonomous systems to increase their robustness, and the value of using bio-inspired engineering to find solutions in this area.

preprint2016arXiv

A Benes Based NoC Switching Architecture for Mixed Criticality Embedded Systems

Multi-core, Mixed Criticality Embedded (MCE) real-time systems require high timing precision and predictability to guarantee there will be no interference between tasks. These guarantees are necessary in application areas such as avionics and automotive, where task interference or missed deadlines could be catastrophic, and safety requirements are strict. In modern multi-core systems, the interconnect becomes a potential point of uncertainty, introducing major challenges in proving behaviour is always within specified constraints, limiting the means of growing system performance to add more tasks, or provide more computational resources to existing tasks. We present MCENoC, a Network-on-Chip (NoC) switching architecture that provides innovations to overcome this with predictable, formally verifiable timing behaviour that is consistent across the whole NoC. We show how the fundamental properties of Benes networks benefit MCE applications and meet our architecture requirements. Using SystemVerilog Assertions (SVA), formal properties are defined that aid the refinement of the specification of the design as well as enabling the implementation to be exhaustively formally verified. We demonstrate the performance of the design in terms of size, throughput and predictability, and discuss the application level considerations needed to exploit this architecture.

preprint2016arXiv

Believing in BERT: Using expressive communication to enhance trust and counteract operational error in physical Human-Robot Interaction

Strategies are necessary to mitigate the impact of unexpected behavior in collaborative robotics, and research to develop solutions is lacking. Our aim here was to explore the benefits of an affective interaction, as opposed to a more efficient, less error prone but non-communicative one. The experiment took the form of an omelet-making task, with a wide range of participants interacting directly with BERT2, a humanoid robot assistant. Having significant implications for design, results suggest that efficiency is not the most important aspect of performance for users; a personable, expressive robot was found to be preferable over a more efficient one, despite a considerable trade off in time taken to perform the task. Our findings also suggest that a robot exhibiting human-like characteristics may make users reluctant to 'hurt its feelings'; they may even lie in order to avoid this.

preprint2016arXiv

ENTRA: Whole-Systems Energy Transparency

Promoting energy efficiency to a first class system design goal is an important research challenge. Although more energy-efficient hardware can be designed, it is software that controls the hardware; for a given system the potential for energy savings is likely to be much greater at the higher levels of abstraction in the system stack. Thus the greatest savings are expected from energy-aware software development, which is the vision of the EU ENTRA project. This article presents the concept of energy transparency as a foundation for energy-aware software development. We show how energy modelling of hardware is combined with static analysis to allow the programmer to understand the energy consumption of a program without executing it, thus enabling exploration of the design space taking energy into consideration. The paper concludes by summarising the current and future challenges identified in the ENTRA project.

preprint2016arXiv

Formal Specification and Analysis of Autonomous Systems under Partial Compliance

The widespread adoption of autonomous systems depends on providing guarantees of safety and functional correctness, at both design time and runtime. Information about the extent to which functional requirements can be met in combination with non-functional requirements (NFRs) -- i.e. requirements that can be partially complied with -- , under dynamic and uncertain environments, provides opportunities to enhance the safety and functional correctness of systems at design time. We present a technique to formally define system attributes that can change or be changed to deal with dynamic and uncertain environments (denominated weakened specifications) as a partially ordered lattice, and to automatically explore the system under different specifications, using probabilistic model checking, to find the likelihood of satisfying a requirement. The resulting probabilities form boundaries of "optimal specifications", analogous to Pareto frontiers in multi-objective optimization, informing the designer about the system's capabilities, such as resilience or robustness, when changing its attributes to deal with dynamic and uncertain environments. We illustrate the proposed technique through a domestic robotic assistant example.

preprint2016arXiv

Model-based Test Generation for Robotic Software: Automata versus Belief-Desire-Intention Agents

Robotic code needs to be verified to ensure its safety and functional correctness, especially when the robot is interacting with people. Testing real code in simulation is a viable option. However, generating tests that cover rare scenarios, as well as exercising most of the code, is a challenge amplified by the complexity of the interactions between the environment and the software. Model-based test generation methods can automate otherwise manual processes and facilitate reaching rare scenarios during testing. In this paper, we compare using Belief-Desire-Intention (BDI) agents as models for test generation with more conventional automata-based techniques that exploit model checking, in terms of practicality, performance, transferability to different scenarios, and exploration (`coverage'), through two case studies: a cooperative manufacturing task, and a home care scenario. The results highlight the advantages of using BDI agents for test generation. BDI agents naturally emulate the agency present in Human-Robot Interactions (HRIs), and are thus more expressive than automata. The performance of the BDI-based test generation is at least as high, and the achieved coverage is higher or equivalent, compared to test generation based on model checking automata.

preprint2016arXiv

Model-Based Testing, Using Belief-Desire-Intentions Agents, of Control Code for Robots in Collaborative Human-Robot Interactions

The software of robotic assistants needs to be verified, to ensure its safety and functional correctness. Testing in simulation allows a high degree of realism in the verification. However, generating tests that cover both interesting foreseen and unforeseen scenarios in human-robot interaction (HRI) tasks, while executing most of the code, remains a challenge. We propose the use of belief-desire-intention (BDI) agents in the test environment, to increase the level of realism and human-like stimulation of simulated robots. Artificial intelligence, such as agent theory, can be exploited for more intelligent test generation. An automated testbench was implemented for a simulation in Robot Operating System (ROS) and Gazebo, of a cooperative table assembly task between a humanoid robot and a person. Requirements were verified for this task, and some unexpected design issues were discovered, leading to possible code improvements. Our results highlight the practicality of BDI agents to automatically generate valid and human-like tests to get high code coverage, compared to hand-written directed tests, pseudorandom generation, and other variants of model-based test generation. Also, BDI agents allow the coverage of combined behaviours of the HRI system with more ease than writing temporal logic properties for model checking.

preprint2015arXiv

A software controlled voltage tuning system using multi-purpose ring oscillators

This paper presents a novel software driven voltage tuning method that utilises multi-purpose Ring Oscillators (ROs) to provide process variation and environment sensitive energy reductions. The proposed technique enables voltage tuning based on the observed frequency of the ROs, taken as a representation of the device speed and used to estimate a safe minimum operating voltage at a given core frequency. A conservative linear relationship between RO frequency and silicon speed is used to approximate the critical path of the processor. Using a multi-purpose RO not specifically implemented for critical path characterisation is a unique approach to voltage tuning. The parameters governing the relationship between RO and silicon speed are obtained through the testing of a sample of processors from different wafer regions. These parameters can then be used on all devices of that model. The tuning method and software control framework is demonstrated on a sample of XMOS XS1-U8A-64 embedded microprocessors, yielding a dynamic power saving of up to 25% with no performance reduction and no negative impact on the real-time constraints of the embedded software running on the processor.

preprint2015arXiv

Coverage-Driven Verification - An approach to verify code for robots that directly interact with humans

Collaborative robots could transform several industries, such as manufacturing and healthcare, but they present a significant challenge to verification. The complex nature of their working environment necessitates testing in realistic detail under a broad range of circumstances. We propose the use of Coverage-Driven Verification (CDV) to meet this challenge. By automating the simulation-based testing process as far as possible, CDV provides an efficient route to coverage closure. We discuss the need, practical considerations, and potential benefits of transferring this approach from microelectronic design verification to the field of human-robot interaction. We demonstrate the validity and feasibility of the proposed approach by constructing a custom CDV testbench and applying it to the verification of an object handover task.

preprint2015arXiv

Evaluating Model Checking Approaches to Verify Stability of Control Systems in Simulink

This paper examines the verification of stability, a control requirement, over discrete control systems represented as Simulink diagrams, using different model checking approaches and tools. Model checking comprises the (exhaustive) exploration of a model of a system, to determine if a requirement is satisfied. If that is not the case, examples of the requirement's violation within the system's model are provided, as witnesses. These examples are potentially complementary to previous work on automatic theorem proving, when a system is not proven to be stable, but no proof of instability can be provided. We experimentally evaluated the suitability of four model checking approaches to verify stability on a set of benchmarks including linear and nonlinear, controlled and uncontrolled, discrete systems, via Lyapunov's second method or Lyapunov's direct method. Our study included symbolic, bounded, statistical and hybrid model checking, through the open-source tools NuSMV, UCLID, S-TaLiRo and SpaceEx, respectively. Our experiments and results provide an insight on the strengths and limitations of these model checking approaches for the verification of control requirements for discrete systems at Simulink level. We found that statistical model checking with S-TaLiRo is the most suitable option to complement our previous work on automatic theorem proving.

preprint2015arXiv

Marimba: A Tool for Verifying Properties of Hidden Markov Models

The formal verification of properties of Hidden Markov Models (HMMs) is highly desirable for gaining confidence in the correctness of the model and the corresponding system. A significant step towards HMM verification was the development by Zhang et al. of a family of logics for verifying HMMs, called POCTL*, and its model checking algorithm. As far as we know, the verification tool we present here is the first one based on Zhang et al.'s approach. As an example of its effective application, we verify properties of a handover task in the context of human-robot interaction. Our tool was implemented in Haskell, and the experimental evaluation was performed using the humanoid robot Bert2.

preprint2015arXiv

Modeling and visualizing networked multi-core embedded software energy consumption

In this report we present a network-level multi-core energy model and a software development process workflow that allows software developers to estimate the energy consumption of multi-core embedded programs. This work focuses on a high performance, cache-less and timing predictable embedded processor architecture, XS1. Prior modelling work is improved to increase accuracy, then extended to be parametric with respect to voltage and frequency scaling (VFS) and then integrated into a larger scale model of a network of interconnected cores. The modelling is supported by enhancements to an open source instruction set simulator to provide the first network timing aware simulations of the target architecture. Simulation based modelling techniques are combined with methods of results presentation to demonstrate how such work can be integrated into a software developer's workflow, enabling the developer to make informed, energy aware coding decisions. A set of single-, multi-threaded and multi-core benchmarks are used to exercise and evaluate the models and provide use case examples for how results can be presented and interpreted. The models all yield accuracy within an average +/-5 % error margin.

preprint2015arXiv

On the Value and Limits of Multi-level Energy Consumption Static Analysis for Deeply Embedded Single and Multi-threaded Programs

There is growing interest in lowering the energy consumption of computation. Energy transparency is a concept that makes a program's energy consumption visible from software to hardware through the different system layers. Such transparency can enable energy optimizations at each layer and between layers, and help both programmers and operating systems make energy aware decisions. The common methodology of extracting the energy consumption of a program is through direct measurement of the target hardware. This usually involves specialized equipment and knowledge most programmers do not have. In this paper, we examine how existing methods for static resource analysis and energy modeling can be utilized to perform Energy Consumption Static Analysis (ECSA) for deeply embedded programs. To investigate this, we have developed ECSA techniques that work at the instruction set level and at a higher level, the LLVM IR, through a novel mapping technique. We apply our ECSA to a comprehensive set of mainly industrial benchmarks, including single-threaded and also multi-threaded embedded programs from two commonly used concurrency patterns, task farms and pipelines. We compare our ECSA results to hardware measurements and predictions obtained based on simulation traces. We discuss a number of application scenarios for which ECSA results can provide energy transparency and conclude with a set of new research questions for future work.

preprint2015arXiv

Static analysis of energy consumption for LLVM IR programs

Energy models can be constructed by characterizing the energy consumed by executing each instruction in a processor's instruction set. This can be used to determine how much energy is required to execute a sequence of assembly instructions, without the need to instrument or measure hardware. However, statically analyzing low-level program structures is hard, and the gap between the high-level program structure and the low-level energy models needs to be bridged. We have developed techniques for performing a static analysis on the intermediate compiler representations of a program. Specifically, we target LLVM IR, a representation used by modern compilers, including Clang. Using these techniques we can automatically infer an estimate of the energy consumed when running a function under different platforms, using different compilers. One of the challenges in doing so is that of determining an energy cost of executing LLVM IR program segments, for which we have developed two different approaches. When this information is used in conjunction with our analysis, we are able to infer energy formulae that characterize the energy consumption for a particular program. This approach can be applied to any languages targeting the LLVM toolchain, including C and XC or architectures such as ARM Cortex-M or XMOS xCORE, with a focus towards embedded platforms. Our techniques are validated on these platforms by comparing the static analysis results to the physical measurements taken from the hardware. Static energy consumption estimation enables energy-aware software development, without requiring hardware knowledge.

preprint2015arXiv

Symmetry Reduction Enables Model Checking of More Complex Emergent Behaviours of Swarm Navigation Algorithms

The emergent global behaviours of robotic swarms are important to achieve their navigation task goals. These emergent behaviours can be verified to assess their correctness, through techniques like model checking. Model checking exhaustively explores all possible behaviours, based on a discrete model of the system, such as a swarm in a grid. A common problem in model checking is the state-space explosion that arises when the states of the model are numerous. We propose a novel implementation of symmetry reduction, in the form of encoding navigation algorithms relatively with respect to a reference, based on the symmetrical properties of swarms in grids. We applied the relative encoding to a swarm navigation algorithm, Alpha, modelled for the NuSMV model checker. A comparison of the state-space and verification results with an absolute (or global) and a relative encoding of the Alpha algorithm highlights the advantages of our approach, allowing model checking larger grid sizes and number of robots, and consequently, verifying more complex emergent behaviours. For example, a property was verified for a grid with 3 robots and a maximum allowed size of 8x8 cells in a global encoding, whereas this size was increased to 16x16 using a relative encoding. Also, the time to verify a property for a swarm of 3 robots in a 6x6 grid was reduced from almost 10 hours to only 7 minutes. Our approach is transferable to other swarm navigation algorithms.

preprint2015arXiv

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

A self-adaptive software system modifies its behavior at runtime in response to changes within the system or in its execution environment. The fulfillment 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 development time, such as design analysis and testing. In the presence of selfadaptation, however, some of the assurance tasks may need to be performed at runtime. This need calls for the development of techniques that enable continuous assurance throughout the software life cycle. Fundamental to the development of runtime assurance techniques is research into the use of models at runtime (M@RT). This chapter explores the state of the art for usingM@RT to address the assurance of self-adaptive software systems. It defines what information can be captured by M@RT, specifically for the purpose of assurance, and puts this definition into the context of existing work. We then outline key research challenges for assurance at runtime and characterize assurance methods. The chapter concludes with an exploration of selected application areas where M@RT could provide significant benefits beyond existing assurance techniques for adaptive systems.

preprint2014arXiv

A high-level model of embedded flash energy consumption

The alignment of code in the flash memory of deeply embedded SoCs can have a large impact on the total energy consumption of a computation. We investigate the effect of code alignment in six SoCs and find that a large proportion of this energy (up to 15% of total SoC energy consumption) can be saved by changes to the alignment. A flexible model is created to predict the read-access energy consumption of flash memory on deeply embedded SoCs, where code is executed in place. This model uses the instruction level memory accesses performed by the processor to calculate the flash energy consumption of a sequence of instructions. We derive the model parameters for five SoCs and validate them. The error is as low as 5%, with a 11% average normalized RMS deviation overall. The scope for using this model to optimize code alignment is explored across a range of benchmarks and SoCs. Analysis shows that over 30% of loops can be better aligned. This can significantly reduce energy while increasing code size by less than 4%. We conclude that this effect has potential as an effective optimization, saving significant energy in deeply embedded SoCs.

preprint2014arXiv

EACOF: A Framework for Providing Energy Transparency to enable Energy-Aware Software Development

Making energy consumption data accessible to software developers is an essential step towards energy efficient software engineering. The presence of various different, bespoke and incompatible, methods of instrumentation to obtain energy readings is currently limiting the widespread use of energy data in software development. This paper presents EACOF, a modular Energy-Aware Computing Framework that provides a layer of abstraction between sources of energy data and the applications that exploit them. EACOF replaces platform specific instrumentation through two APIs - one accepts input to the framework while the other provides access to application software. This allows developers to profile their code for energy consumption in an easy and portable manner using simple API calls. We outline the design of our framework and provide details of the API functionality. In a use case, where we investigate the impact of data bit width on the energy consumption of various sorting algorithms, we demonstrate that the data obtained using EACOF provides interesting, sometimes counter-intuitive, insights. All the code is available online under an open source license. http://github.com/eacof

preprint2014arXiv

Formal Verification of Control Systems Properties with Theorem Proving

This paper presents the deductive formal verification of high-level properties of control systems with theorem proving, using the Why3 tool. Properties that can be verified with this approach include stability, feedback gain, and robustness, among others. For the systems, modelled in Simulink, we propose three main steps to achieve the verification: specifying the properties of interest over the signals within the model using Simulink blocks, an automatic translation of the model into Why3, and the automatic verification of the properties with theorem provers in Why3. We present a methodology to specify the properties in the model and a library of relevant assertion blocks (logic expressions), currently in development. The functionality of the blocks in the Simulink models are automatically translated to Why3 as theories and verification goals by our tool implemented in MATLAB. A library of theories in Why3 corresponding to each supported block has been developed to facilitate the process of translation. The goals are automatically verified in Why3 with relevant theorem provers. A simple first-order discrete system is used to exemplify the specification of the Simulink model, the translation process from Simulink to the Why3 formal logic language, and the verification of Lyapunov stability.