Integrating hardware and software information flow analyses

Security-critical communications devices must be evaluated to the highest possible standards before they can be deployed. This process includes tracing potential information flow through the device's electronic circuitry, for each of the device's operating modes. Increasingly, however, security functionality is being entrusted to embedded software running on microprocessors within such devices, so new strategies are needed for integrating information flow analyses of embedded program code with hardware analyses. Here we show how standard compiler principles can augment high-integrity security evaluations to allow seamless tracing of information flow through both the hardware and software of embedded systems. This is done by unifying input/output statements in embedded program execution paths with the hardware pins they access, and by associating significant software states with corresponding operating modes of the surrounding electronic circuitry.

Stepwise refinement of interrupt-driven real-time programs

Embedded real-time programs rely on external interrupts to respond to events in their physical environment in a timely fashion. Formal program verification theories, such as the refinement calculus, are intended for development of sequential, block-structured code and do not allow for asynchronous control constructs such as interrupt service routines. In this article we extend the refinement calculus to support formal development of interrupt-dependent programs. To do this we: use a timed semantics, to support reasoning about the occurrence of interrupts within bounded time intervals; introduce a restricted form of concurrency, to model composition of interrupt service routines with the main program they may preempt; introduce a semantics for shared variables, to model contention for variables accessed by both interrupt service routines and the main program; and use real-time scheduling theory to discharge timing requirements on interruptible program code.

How to design extended finite state machine test models in Java

This chapter is a tutorial that teaches you how to design extended finite state machine (EFSM) test models for a system that you want to test. EFSM models are more powerful and expressive than simple finite state machine (FSM) models, and are one of the most commonly used styles of models for model-based testing, especially for embedded systems. There are many languages and notations in use for writing EFSM models, but in this tutorial we write our EFSM models in the familiar Java programming language. To generate tests from these EFSM models we use ModelJUnit, which is an open-source tool that supports several stochastic test generation algorithms, and we also show how to write your own model-based testing tool. We show how EFSM models can be used for unit testing and system testing of embedded systems, and for offline testing as well as online testing.

Multi-level information fusion for environment aware robotic navigation

This thesis develops the hardware and software framework for an integrated navigation system. Dynamic data fusion algorithms are used to develop a system with a high level of resistance to the typical problems that affect standard navigation systems.

Dynamic robot path planning using an enhanced simulated annealing approach

Evolutionary computation is an effective tool for solving optimization problems. However, its significant computational demand has limited its real-time and on-line applications, especially in embedded systems with limited computing resources, e.g., mobile robots. Heuristic methods such as the genetic algorithm (GA) based approaches have been investigated for robot path planning in dynamic environments. However, research on the simulated annealing (SA) algorithm, another popular evolutionary computation algorithm, for dynamic path planning is still limited mainly due to its high computational demand. An enhanced SA approach, which integrates two additional mathematical operators and initial path selection heuristics into the standard SA, is developed in this work for robot path planning in dynamic environments with both static and dynamic obstacles. It improves the computing performance of the standard SA significantly while giving an optimal or near-optimal robot path solution, making its real-time and on-line applications possible. Using the classic and deterministic Dijkstra algorithm as a benchmark, comprehensive case studies are carried out to demonstrate the performance of the enhanced SA and other SA algorithms in various dynamic path planning scenarios.

Remote sensing utility expansion through Earth Portal internet browser

A modular, graphic-oriented Internet browser has been developed to enable non-technical client access to a literal spinning world of information and remotely sensed. The Earth Portal (www.earthportal.net) uses the ManyOne browser (www.manyone.net) to provide engaging point and click views of the Earth fully tessellated with remotely sensed imagery and geospatial data. The ManyOne browser technology use Mozilla with embedded plugins to apply multiple 3-D graphics engines, e.g. ArcGlobe or GeoFusion, that directly link with the open-systems architecture of the geo-spatial infrastructure. This innovation allows for rendering of satellite imagery directly over the Earth's surface and requires no technical training by the web user. Effective use of this global distribution system for the remote sensing community requires a minimal compliance with protocols and standards that have been promoted by NSDI and other open-systems standards organizations.

ICEPOLE: High-speed, hardware-oriented authenticated encryption

This paper introduces our dedicated authenticated encryption scheme ICEPOLE. ICEPOLE is a high-speed hardware-oriented scheme, suitable for high-throughput network nodes or generally any environment where specialized hardware (such as FPGAs or ASICs) can be used to provide high data processing rates. ICEPOLE-128 (the primary ICEPOLE variant) is very fast. On the modern FPGA device Virtex 6, a basic iterative architecture of ICEPOLE reaches 41 Gbits/s, which is over 10 times faster than the equivalent implementation of AES-128-GCM. The throughput-to-area ratio is also substantially better when compared to AES-128-GCM. We have carefully examined the security of the algorithm through a range of cryptanalytic techniques and our findings indicate that ICEPOLE offers high security level.

In bed with technology: Challenges and opportunities for sleep tracking

In recent years a variety of mobile apps, wearable technologies and embedded systems have emerged that allow individuals to track the amount and the quality of their sleep in their own beds. Despite the widespread adoption of these technologies, little is known about the challenges that current users face in tracking and analysing their sleep. Hence we conducted a qualitative study to examine the practices of current users of sleep tracking technologies and to identify challenges in current practice. Based on data collected from 5 online forums for users of sleep-tracking technologies, we identified 22 different challenges under the following 4 themes: tracking continuity, trust, data manipulation, and data interpretation. Based on these results, we propose 6 design opportunities to assist researchers and practitioners in designing sleep-tracking technologies.

System-level analysis of network interfaces for hierarchical MPSoCs

Network Interfaces (NIs) are used in Multiprocessor System-on-Chips (MPSoCs) to connect CPUs to a packet switched Network-on-Chip. In this work we introduce a new NI architecture for our hierarchical CoreVA-MPSoC. The CoreVA-MPSoC targets streaming applications in embedded systems. The main contribution of this paper is a system-level analysis of different NI configurations, considering both software and hardware costs for NoC communication. Different configurations of the NI are compared using a benchmark suite of 10 streaming applications. The best performing NI configuration shows an average speedup of 20 for a CoreVA-MPSoC with 32 CPUs compared to a single CPU. Furthermore, we present physical implementation results using a 28 nm FD-SOI standard cell technology. A hierarchical MPSoC with 8 CPU clusters and 4 CPUs in each cluster running at 800MHz requires an area of 4.56mm2.

An examination of the knowledge barriers in participatory design and the prospects for embedded research

Participatory design has the moral and pragmatic tenet of including those who will be most affected by a design into the design process. However, good participation is hard to achieve and results linking project success and degree of participation are inconsistent. Through three case studies examining some of the challenges that different properties of knowledge - novelty, difference, dependence - can impose on the participatory endeavour we examine some of the consequences to the participatory process of failing to bridge across knowledge boundaries - syntactic, semantic, and pragmatic. One pragmatic consequence, disrupting the user's feeling of involvement to the project, has been suggested as a possible explanation for the inconsistent results linking participation and project success. To aid in addressing these issues a new form of participatory research, called embedded research, is proposed and examined within the framework of the case studies and knowledge framework with a call for future research into its possibilities.

SSE based parallel solution for power systems network equations

Streaming SIMD Extensions (SSE) is a unique feature embedded in the Pentium III class of microprocessors. By fully exploiting SSE, parallel algorithms can be implemented on a standard personal computer and a theoretical speedup of four can be achieved. In this paper, we demonstrate the implementation of a parallel LU matrix decomposition algorithm for solving power systems network equations with SSE and discuss advantages and disadvantages of this approach.

A parallel solution to linear systems

Streaming SIMD Extensions (SSE) is a unique feature embedded in the Pentium III and IV classes of microprocessors. By fully exploiting SSE, parallel algorithms can be implemented on a standard personal computer and a theoretical speedup of four can be achieved. In this paper, we demonstrate the implementation of a parallel LU matrix decomposition algorithm for solving linear systems with SSE and discuss advantages and disadvantages of this approach based on our experimental study.

Seismic mitigation of building structural systems using passive dampers

This paper treats the seismic mitigation of medium rise frame-shear wall structures and building facade systems using passive damping devices. The frame shear wall structures have embedded viscoelastic and friction dampers in different configurations and placed in various locations in the structure. Influence of damper type, configuration and location are investigated. Results for tip deflections which provide an overall evaluation of the seismic response of the structure, are determined. Seismic mitigation of building facade systems in which visco-elastic dampers are fitted at the horizontal connections between the facades and the frame, instead of the traditional rigid connections, are also treated. Finite element techniques are used to model and analyse the two structural systems under different earthquake loadings, scaled to the same peak ground acceleration for meaningful comparison of responses. Results demonstrate the feasibility of these techniques for seismic mitigation.