Real-time systems are a segment of embedded systems that have remained dominated by proprietary hardware architectures, despite the continuing growth of the open-source RISC-V instruction set architecture (ISA). The introduction of core-local interrupt controller (CLIC) extensions to the RISC-V architecture presents a promising opportunity to bridge the technological gap with ARM in low-latency interrupt handling. Regarding software, the real-time interrupt-driven concurrency (RTIC) framework enables ever lighter hard real-time systems with formal compile-time guarantees for memory safety, response time and overall schedulability. In this publication we adapt Ibex, a small, open-source RISC-V processor for CLIC support and present Atalanta, a lightweight microcontroller designed around the RTIC framework. Atalanta implements a localized memory architecture that enables low-latency context switching together with a large number of supported interrupt inputs and levels provided by the CLIC specification. We evaluate Atalanta for real-time performance and implementation feasibility through simulation-based measurements and FPGA prototyping, respectively. We are able to demonstrate an interrupt latency of 5 cycles with minimal jitter and a context switch latency of 21 cycles, placing it competitively against current state-of-the-art solutions. Furthermore, we implement an FPGA prototype for the Xilinx PYNQ-Z1 and VCU118 boards, targeting a frequency of 45 MHz. We publish the sources and implementation scripts of Atalanta under a permissive open-source license.

Memory safety is instrumental to the safety and security of software systems. The Rust language stands out with a type system and underlying memory model targeting memory safety without the need for dynamic garbage collection, making Rust a viable option for embedded applications. In this paper we present an integrated tool for call-stack analysis of Rust applications. We cover both theoretical and practical challenges, their solutions and open questions. The cargo-call-stack tool is useful for analyzing Rust applications in general, and embedded Rust in particular. To the latter, we show that using the call-stack analysis we can give guarantees of total memory safety, free of assumptions on operating systems and underlying memory protection mechanisms in hardware. The feasibility of the approach is demonstrated by applying the `call-stack' tool on production code targeting a light-weight ARM Cortex-M platform.

Embedded systems of the IoT era face the software developer with requirements on a mix of resource efficiency, real-time, safety, and security properties. As of today, C/C++ programming dominates the mainstream of embedded development, which leaves ensuring system wide properties mainly at the hands of the programmer. We adopt a programming model and accompanying framework implementation that leverages on the memory model, type system, and zero-cost abstractions of the Rust language. Based on the outset of reactivity, a software developer models a system in terms of Concurrent Reactive Objects (CROs) hierarchically grouped into Concurrent Reactive Components (CRCs) with communication captured in terms of time constrained synchronous and asynchronous messages. The developer declaratively defines the system, from which a static system instance can be derived and analyzed. A system designed in the proposed CRC framework has the outstanding properties of efficient, memory safe, race-, and deadlock-free preemptive (single-core) execution with predictable real-time properties. In this paper, we further explore the Rust memory model and the CRC framework towards systems being secure by construction. In particular, we show that permissions granted can be freely delegated without any risk of leakage outside the intended set of components. Moreover, the model guarantees permissions to be authentic, i.e., neither manipulated nor faked. Finally, the model guarantees permissions to be temporal, i.e., never to outlive the granted authority. We believe and argue that these properties offer the fundamental primitives for building secure by construction applications and demonstrate its feasibility on a small case study, a wireless autonomous system based on an ARM Cortex M3 target.

Classes on compiler technology are commonly found in Computer Science curricula, covering aspects of parsing, semantic analysis, intermediate transformations and target code generation. This paper reports on introducing certified compilation techniques through a functional language approach in an introductory course on Compiler Construction. Targeting students with little or no experience in formal methods, the proof process is highly automated using the Why3 framework. Underlying logic, semantic modelling and proofs are introduced along with exercises and assignments leading up to a formally verified compiler for a simplistic imperative language.

This paper covers the motivation, course design, tool selection, and teaching methods, together with evaluations and suggested improvements from the perspectives of both students and teachers.