Safety-critical embedded systems, commonly found in automotive, space, and health-care, are highly reactive and concurrent. Their most important characteristics are that they require both functional and timing correctness. C has been the language of choice for programming such systems. However, C lacks many features that can make the design process of such systems seamless while also maintaining predictability. This paper addresses the need for a C-based design framework for achieving time predictability. To this end, we propose the PRET-C language and the ARPRET architecture. PRET-C offers a small set of extensions to a subset of C to facilitate effective concurrent programming. We present a new synchronous semantics for PRET-C. It guarantees that all PRET-C programs are deterministic, reactive, and provides thread-safe communication via shared memory access. This simplifies considerably the design of safety-critical systems. We also present the architecture of a precision timed machine (PRET) called ARPRET. It offers the ability to design time predictable architectures through simple customizations of soft-core processors. We have designed ARPRET particularly for efficient and predictable execution of PRET-C. We demonstrate through extensive benchmarking that PRET-C based system design excels in comparison to existing C-based paradigms. We also qualitatively compare our approach to the Berkeley-Columbia PRET approach. We have demonstrated that the proposed approach provides an ideal framework for designing and validating safety-critical embedded systems.

SyncCharts are a synchronous Statechart variant to model reactive systems with a precise and deterministic semantics. The simulation and software synthesis for SyncCharts usually involve the compilation into Esterel, which is then further compiled into C code. This can produce efficient code, but has two principal drawbacks: 1) the arbitrary control flow that can be expressed with SyncChart transitions cannot be mapped directly to Esterel, and 2) it is very difficult to map the resulting C code back to the original SyncChart, which hampers traceability. This paper presents an alternative software synthesis approach for SyncCharts that compiles SyncCharts directly into Synchronous C (SC). The compilation preserves the structure of the original SyncChart, which is advantageous for validation and possibly certification. We present a static thread-scheduling scheme that reflects data dependencies and optimizes both the number of used threads as well as the maximal used priorities. This results in SC code with competitive speed and little memory requirements.

Accurate estimation of the tick length of a synchronous program is essential for efficient and predictable implementations that are devoid of timing faults. The techniques to determine the tick length statically are classified as worst case reaction time (WCRT) analysis. While a plethora of techniques exist for worst case execution time (WCET) analysis of procedural programs, there are only a handful of techniques for determining the WCRT value of synchronous programs. Most of these techniques produce overestimates and hence are unsuitable for the design of systems that are predictable while being also efficient. In this paper, we present an approach for the accurate estimation of the exact WCRT value of a synchronous program, called its tight WCRT value, using model checking. For our input specifications we have selected a synchronous C based language called PRET-C that is designed for programming Precision Timed (PRET) architectures. We then present an approach for static WCRT analysis of these programs via an intermediate format called TCCFG. This intermediate representation is then compiled to produce the input for the model checker.

The synchronous model of computation together with a suitable execution platform facilitates system-level timing predictability. This paper introduces an algebraic framework for precisely capturing worst case reaction time (WCRT) characteristics for Esterel-style reactive processors with hardware-supported multithreading. This framework provides a formal grounding for the WCRT problem, and allows to improve upon earlier heuristics by accurately and modularly characterizing timing interfaces.

Esterel and Safe State Machines (SSMs) are synchronous languages dedicated to the modeling of embedded reactive systems. While Esterel is a textual language, SSMs are based on the graphical Statecharts formalism. Statecharts are often more intuitive to understand than their textual counterpart, and their animated simulation can help to visualize subtle behaviors of a program. However, in terms of editing speed, revision management, and meta-modeling, the textual nature of Esterel is advantageous. We present an approach to transform Esterel v5 programs into equivalent SSMs. This permits a design flow where the designer develops a system at the Esterel level, but uses a graphical browser and simulator to inspect and validate the system under development.We synthesize SSMs in two phases. The first phase transforms an Esterel program into an equivalent SSM, using a structural translation that results in correct, but typically not very compact SSMs. The second phase iteratively applies optimization rules that aim to reduce the number of states, transitions and hierarchy levels to enhance readability of the SSM. As it turned out, this optimization is also useful for the traditional, manual design of SSMs. The complete transformation has been implemented in a prototypical modeling environment, which allows to demonstrate the practicality of this approach and the compactness of the generated SSMs.