Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce the novel Hoare-style program logic L A , which interprets postconditions relative to program points when these are first encountered. The logic supports both partial and total correctness, derives contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of L A have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, which supports the ARMv6, ARMv8 and RISC-V instruction sets.

Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening (slh) in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using slh that often results in over-protection, which incurs performance overhead. We extended an existing side-channel model validation framework, Scam-V, to check the vulnerability of programs to Spectre-PHT attacks and optimize the protection of programs using the slh approach. We illustrate the efficacy of Scam-V by first demonstrating that it can automatically identify Spectre vulnerabilities in programs, e.g., fragments of crypto-libraries. We then develop an optimization mechanism to validate the necessity of slh hardening w.r.t. the target platform. Our experiments showed that hardening introduced by LLVM in most cases could be improved when the underlying microarchitecture properties are considered.

MOTIVATION: Multiplexed immunofluorescence bioimaging of single-cells and their spatial organization in tissue holds great promise to the development of future precision diagnostics and therapeutics. Current multiplexing pipelines typically involve multiple rounds of immunofluorescence staining across multiple tissue slides. This introduces experimental batch effects that can hide underlying biological signal. It is important to have robust algorithms that can correct for the batch effects while not introducing biases into the data. Performance of data normalization methods can vary among different assay pipelines. To evaluate differences, it is critical to have a ground truth dataset that is representative of the assay. RESULTS: A new immunoFLuorescence Image NOrmalization method is presented and evaluated against alternative methods and workflows. Multiround immunofluorescence staining of the same tissue with the nuclear dye DAPI was used to represent virtual slides and a ground truth. DAPI was restained on a given tissue slide producing multiple images of the same underlying structure but undergoing multiple representative tissue handling steps. This ground truth dataset was used to evaluate and compare multiple normalization methods including median, quantile, smooth quantile, median ratio normalization and trimmed mean of the M-values. These methods were applied in both an unbiased grid object and segmented cell object workflow to 24 multiplexed biomarkers. An upper quartile normalization of grid objects in log space was found to obtain almost equivalent performance to directly normalizing segmented cell objects by the middle quantile. The developed grid-based technique was then applied with on-slide controls for evaluation. Using five or fewer controls per slide can introduce biases into the data. Ten or more on-slide controls were able to robustly correct for batch effects. AVAILABILITY AND IMPLEMENTATION: The data underlying this article along with the FLINO R-scripts used to perform the evaluation of image normalizations methods and workflows can be downloaded from https://github.com/GE-Bio/FLINO. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

Observational models enable the analysis of information flow properties against side channels. Relational testing has been used to validate the soundness of these models by measuring the side channel on states that the model considers indistinguishable. However, unguided search can generate test states that are too similar to each other to invalidate the model. To address this we introduce observation refinement, a technique to guide the exploration of the state space to focus on hardware features of interest. We refine observational models to include fine-grained observations that characterize behavior that we want to exclude. States that yield equivalent refined observations are then ruled out, reducing the size of the space. We have extended an existing model validation framework, Scam-V, to support refinement. We have evaluated the usefulness of refinement for search guidance by analyzing cache coloring and speculative leakage in the ARMv8-A architecture. As a surprising result, we have exposed SiSCLoak, a new vulnerability linked to speculative execution in Cortex-A53.

Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior.

The work discusses and finally verifies the working principle of a passive stator cooling concept employing conventional heat pipes. For this purpose a test-setup based on a small power medium speed 6/8-flux-switching permanent magnet machine with an extraordinarily large air-gap of δ=4 mm is manufactured, commissioned and measurements are recorded proving the concept of both: the electromagnetic machine design and particularly the passive stator cooling concept. The elegance of the presented passive cooling principle especially lies in easy adaptability on an existing electrical machine which is already in service, its simple structure, minor requirements of additional cooling equipment and its cooling capabilities. However, some limitation in the maximum dissipatable power and manufacturing are experienced as well.

The IEC 61499 standard provides means to specify distributed control systems in terms of function blocks. For the deployment, each device may hold one or many logical resources, each consisting of a function block network with service interface blocks at the edges. The execution model is event driven (asynchronous), where triggering events may be associated with data (and seen as messages). In this paper, we propose a low-complexity implementation technique allowing to assess end-to-end response times of event chains spanning over a set of networked devices. Based on a translation of IEC 61499 to RTFM11Real-time for the masses.

Embedded systems for critical applications are typically specified with requirements on predictable timing and safety. While ensuring predictable timing, the RTFM-lang (Real-Time For the Masses) model of computation (MoC) currently lacks memory access protection among real-time tasks. In this paper, we discuss how to safely verify task execution given a specification using the RTFM-MoC. Furthermore, an extension to the RTFM-core infrastructure is outlined and tested with use cases of embedded development. We propose a method for run time verification exploiting memory protection hardware. For this purpose, we introduce memory resources to the declarative language RTFM-core allowing compliance checks. As a proof of concept, compiler support for model analysis and automatic generation of run time verification code is implemented together with an isolation layer for the RTFM-kernel. With this verification foundation, functional run time checks as well as further overhead assessments are future research questions.

The work presents two alternative ways of cooling a flux-switching permanent magnet machine with a large air-gap length of 3 mm. The investigations are based on a small power machine (DSa= 100 mm, l = 80 mm) which is designed for the needs of a special application where a defined clearance between the stator and rotor is required to ensure the working principle. The increased air-gap volume promotes the machine cooling from the stator inner surface by means of applying ordinary rotor (step) skewing technique for the salient pole reluctance rotor. In order to proof this cooling concept a test-setup is build up for thermal evaluation purposes. A more widely applicable approach for the thermal heat dissipation within the machine stator is also presented. In this case, the heat is directly extracted from the coil sides of the stator phase winding employing heat pipes. This totally passive cooling technique can improve the efficiency of all kinds of machines by keeping the phase resistance at lower levels or alternatively allowing an increase of current density in the slot without the need of additional cooling equipment like a fan, a radiator or a liquid cooling circuit.

The IEC 61499 standard provides an executable model for distributed control systems in terms of interacting function blocks. However, the current IEC 61499 standard lacks appropriate timing semantics for the specification of timing requirements, reasoning on timing properties at the model level, and for the timing verification of a specific deployment. In this paper we address this fundamental shortcoming by proposing Real-Time-4-FUN, a real-time semantics for IEC 61499. The key property is the preservation of non-determinism, allowing us to reason on (and verify) timing properties at the model level without assuming any specific scheduling policy or stipulating specific order of execution for the deployment. This provides for a clear separation of concerns, where the designer can focus on properties of the application prior to, and separately from, deployment verification. The proposed timing semantics is backwards compatible to the current standard, thus allow for reuse of existing designs. The transitional property allows timing requirements to propagate to downstream sub-systems, and can be utilized for scheduling both at device and network level. Based on a translation to RTFM-tasks and resources, IEC 61499 models can be analyzed, compiled and executed. As a proof of concept the timing semantics has been experimentally implemented in the RTFM-core language and the accompanying (thread based) RTFM-RT run-time system.

The IEC 61449 standard provides an outset for designing and deploying distributed control systems. Recently, a mapping from IEC 61499 to the RTFM-kernel API has been presented. This allows predictable real-time execution of IEC 61499 applications on light-weight single-core platforms. However, integrating the RTFM-kernel (bare-metal runtime) into potential deployments requires developing device drivers, protocol stacks, and the like. For this presentation, we apply the mapping from IEC 61499 to the RTFM-MoC task and resource model implemented by the RTFM-core language. The compilation from RTFM-core can be targeted to both, RTFM-kernel and the introduced runtime system RTFM-RT. In this paper, we detail the generic RTFM-RT runtime architecture, which allows RTFM-core programs to be executed on top of thread based environments. Furthermore, we discuss our implementation regarding scheduling specifics of Win32 threads (Windows) and Pthreads (Linux and Mac OS X). Using our RTFM-RT implementation for deployment, predictable IEC 61499 execution together with access to abovementioned operating system functions are achieved. For further developments, we discuss the needed scheduling options to achieve hard real-time and analysis required to eliminate deadlocks.

The IEC 61499 standard provides means to specify distributed control systems in terms of function blocks. The execution model is event driven (asynchronous), where triggering events may be associated with data (and seen as a message). In this paper we propose a low complexity implementation technique allowing to assess end-to-end response time of event chains spanning over a set of networked devices. In this paper we develop a method to provide safe end-to-end response time taking both intra- and inter-device delivery delays into account. As a use case we study the implementation onto (single-core) ARM-cortex based devices communicating over a switched Ethernet network. For the analysis we define a generic switch model and an experimental setup allowing us to study the impact of network topology as well as 802.1Q quality of service in a mixed critical setting. Our results indicate that safe sub millisecond end-to-end response times can be obtained using the proposed approach.

The mainstream of embedded software development as of today is dominated by C programming. To aid the development, hardware abstractions, libraries, kernels and lightweight operating systems are commonplace. Such kernels and operating systems typically impose a thread based abstraction to concurrency. However, in general thread based programming is hard, plagued by race conditions and dead-locks. For this paper we take an alternative outset in terms of a language abstraction, RTFM-core, where the system is modelled directly in terms of tasks and resources. In compliance to the Stack Resource Policy (SRP) model, the language enforces (well-formed) LIFO nesting of claimed resources, thus SRP based analysis and scheduling can be readily applied. For the execution onto bare-metal single core architectures, the rtfm-core compiler performs SRP analysis on the model and render an executable that is deadlock free and (through RTFM-kernel primitives) exploits the underlying interrupt hardware for efficient scheduling. The RTFM-core language embeds C-code and links to C-object files and libraries, and is thus applicable to the mainstream of embedded development. However, while the language enforces well-formed resource management, control flow in the embedded C-code may violate the LIFO nesting requirement. In this paper we address this issue by lifting a subset of C into the RTFM-core language allowing arbitrary control flow at the model level. In this way well-formed LIFO nesting can be enforced, and models ensured to be correct by construction. We demonstrate the feasibility by means of a prototype implementation in the rtfm-core compiler. Additionally, we develop a set of running examples and show in detail how control flow is handled at compile time and during run-time execution.

Function Blocks provides a means to model and program industrial control systems. The recently acclaimed IEC 61499 standard allows such system models to be partitioned and executed in a distributed fashion. At device level, such models are traditionally implemented onto programmable logic controllers that underneath have an operating system and a software run-time environment which implies high resource demands. However, there is a current trend to involve small embedded systems (so called Internet of Things devices) integrated into such distributed control systems. To this end, we seek to address the outsets for real-time execution of Function Block based designs onto light-weight controllers (MCUs) with limited resources (memory and CPU). Furthermore, we propose a mapping of the Function Block execution semantics onto the RTFM-kernel, and discuss opportunities for off-line (design time) analysis with respect to response time, overall schedulability and memory requirements.

A small size flux-switching permanent magnet machine is designed by means of finite element analysis having a concentrated toroidal winding in the stator and a large air-gap. The design concept is compared to a C-core flux-switching machine having the same magnet volume. Simulation shows that the electromagnetic performance of the toroidal wound FSPM is lower in the first place because of the different winding configuration. However a better cooling of the stator winding is possible so that at full load operation the temperature rise of the winding can be better limited.

This manuscript describes the identification process of the parameters of the Jiles-Atherton-model (JAM) which can be used to characterize the magnetic behavior of electrical steel sheets. A simple semi-analytic parameter identification process using only a small set of symmetrical hysteresis loops is proposed, which requires low computational effort in contrast to the intensive numerical optimization algorithms which are normally used to gain the JAM parameters. Finally some aspects concerning the representation of minor loops will be discussed.

This paper describes a unifying data management concept for feedback assistance systems. The assistance system is to be integrated into existing system scenery. During the use of a hydraulic system, objective feedback such as sensor data or service data is captured and managed in local databases by the machine operators. The aim is to lead such Product Use Information (PUI) back into product development. That way, the product developer uses the information to derive additional and innovative potential to improve next generation products. The information flow is related in various systems i.e. the operator of the machine and the manufacturer. Furthermore, the PUI is managed inside the assistance system based on a data warehouse. The data warehouse is coupled with a Product Lifecycle Management (PLM) system, a well-known system to product developers. Within the PLM system, product master data is created and managed. This also serves as the basis for the assistance system, so that the data models for both systems have to be amalgamated.