Abstract
Robustness, real-time properties and resource efficiency are key properties to embedded devices of the CPS/IoT era. In this paper we propose a language approach RTFM-core, and show its potential to facilitate the development process and provide highly efficient and statically verifiable implementations. Our programming model is reactive, based on the familiar notions of concurrent tasks and (single-unit) resources. The language is kept minimalistic, capturing the static task, communication and resource structure of the system. Whereas C-source can be arbitrarily embedded in the model, and/or externally referenced, the instep to mainstream development is minimal, and a smooth transition of legacy code is possible. A prototype compiler implementation for RTFM-core is presented. The compiler generates C-code output that compiled together with the RTFM-kernel primitives runs on bare metal. The RTFM-kernel guarantees deadlock-lock free execution and efficiently exploits the underlying interrupt hardware for static priority scheduling and resource management under the Stack Resource Policy. This allows a plethora of well-known methods to static verification (response time analysis, stack memory analysis, etc.) to be readily applied. The proposed language and supporting tool-chain is demonstrated by showing the complete process from RTFM-core source code into bare metal executables for a lightweight ARM-Cortex M3 target.

Abstract
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. © 2015 IEEE.

Abstract
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. © 2015 IEEE.

Abstract
The Ada language has for long provided support for the development of reliable real-time systems, with a model of computation amenable for real-time analysis. To complement the already existent multiprocessor support in the language, an ongoing effort is underway to extend Ada with a fine-grained parallel programming model also suitable for real-time systems. This paper overviews the model which is being proposed, pointing out the main issues still open and road ahead. © 2015 IEEE.

Abstract
Many embedded multi-core systems incorporate both dataflow applications with timing constraints and traditional real-time applications. Applying real-time scheduling techniques on such systems provides real-time guarantees that all running applications will execute safely without violating their deadlines. However, to apply traditional real-time scheduling techniques on such mixed systems, a unified model to represent both types of applications running on the system is required. Several earlier works have addressed this problem and solutions have been proposed that address acyclic graphs, implicit-deadline models or are able to extract timing parameters considering specific scheduling algorithms. In this paper, we present an algorithm for extracting real-time parameters (offsets, deadlines and periods) that are independent of the schedulability analysis, other applications running in the system, and the specific platform. The proposed algorithm: 1) enables applying traditional real-time schedulers and analysis techniques on cyclic or acyclic Homogeneous Synchronous Dataflow (HSDF) applications with periodic sources, 2) captures overlapping iterations, which is a main characteristic of the execution of dataflow applications, 3) provides a method to assign offsets and individual deadlines for HSDF actors, and 4) is compatible with widely used deadline assignment techniques, such as NORM and PURE. The paper proves the correctness of the proposed algorithm through formal proofs and examples.

Abstract
The IEC 61499 standard proposes an event driven execution model for distributed control applications for which an informal execution semantics is provided. Consequently, run-time implementations are not rigorously described and therefore their behavior relies on the interpretation made by the tool provider. In this paper, as a step towards a formal semantics, we focus on the Execution Control Chart semantics, which is fundamental to the dynamic behavior of Basic Function Block elements. In particular we develop a well-formedness criterion that ensures a finite number of Execution Control Chart transitions for each triggering event. We also describe the first step towards the mechanization of the well-formedness checking algorithm in the Coq proof-assistant so that, ultimately, we are able to show, once and for all, that this algorithm is effectively correct with respect to our proposed execution semantics. The algorithm is extractable from the mechanization in a correct-by-construction way, and can be directly incorporated in certified toolchain for analysis, compilation and execution of IEC 61499 models. As a proof of concept a prototype tool RTFM-4FUN has been developed. It performs well-formedness checks on Basic Function Blocks using the extracted algorithm's code.