The correctness of a real-time system depends both on it being logically sound and temporally correct. To guarantee temporal correctness, the development of such systems includes: (i) developing a model, (ii) formally verifying the model, and (iii) implementing the verified model using a programming language. The temporal correctness then depends on correctly implementing the model using a real-time programming language and compiling it to a hardware platform. Although the timing semantics of many real-time programming languages are well defined, there is no guarantee that the timing semantics of such programs are correctly translated by the compiler. In this paper, we propose a new method for temporal property-based testing. The general method is implemented and evaluated on the Timed C real-time programming language. We formalize the temporal core semantics of Timed C and then use this formalization to specify the properties that are tested by the new property-based testing tool. More specifically, the tool consist of two parts: (i) a generator that randomly generates Timed C programs, and (ii) a property checker that checks whether the language's timing semantics are correctly captured in its execution. We evaluate the method and tool on an embedded Raspberry Pi platform.

Complex real-time systems are traditionally developed in several disjoint steps: (i) decomposition of applications into sets of recurrent tasks, (ii) worst-case execution time estimation, and (iii) schedulability analysis. Each step is already in itself complex and error-prone, and the composition of all three poses a nontrivial integration problem. In particular, it is challenging to obtain an end-to-end analysis of timing properties of the whole system due to practical differences between the interfaces of tools for extracting task models, execution time analysis, and schedulability tests. To address this problem, we propose a seamless and pragmatic end-to-end compilation and timing analysis toolchain, where source programs are written in a real-time extension of C, called Timed C. The toolchain automatically translates timing primitives into executable code, measures execution times, and verifies temporal correctness using an extended schedulability test for non-preemptive generalized multiframe task sets. Novel aspects of our approach are: (i) both soft and firm tasks can be expressed at the programming language level and stated timing requirements are automatically verified by the schedulability test, and (ii) the schedulability test outputs per-job response-time information that enables a new approach to sensitivity analysis. Specifically, we perform a weakly hard sensitivity analysis that determines the worst-case execution time margins for the strongest still-satisfied (M,K) constraint, where M = m1+...+ mNdenotes the number of deadline misses across the entire task set, and K = {k1,..., kN} is the set of windows of interest of the different tasks. The toolchain is implemented as a source-to-source compiler, freely available as open source, and conveniently distributed as a Docker container.

The design and implementation of real-time systems require that both the logical and the temporal behavior are correct. There exist several specialized languages and tools that use the notion of logical time, as well as industrial strength languages such as Ada and RTJS that incorporate direct handling of real time. Although these languages and tools have shown to be good alternatives for safety-critical systems, most commodity real-time and embedded systems are today implemented in the standard C programming language. Such systems are typically targeting proprietary bare-metal platforms, standard POSIX compliant platforms, or open-source operating systems. It is, however, error prone to develop large, reliable, and portable systems based on these APIs. In this paper, we present an extension to the C programming language, called Timed C, with a minimal set of language primitives, and show how a retargetable source-to-source compiler can be used to compile and execute simple, expressive, and portable programs. To evaluate our approach, we conduct a case study of a CubeSat satellite. We implement the core timing aspects in Timed C, and show portability by compiling on-board software to both flight hardware, and to low-cost experimental platforms.