Home | Research | Enseignement | Prelude

Prelude: programming critical real-time systems

To cite this work, please cite this or this.

Further references available here.

Introduction

Prelude is a high-level language for programming real-time embedded control systems. It is built upon Synchronous Languages (such as Lustre) and inherits their formal properties. It adds real-time primitives to enable the programming of multi-periodic systems. The objective of the language is not to replace other synchronous languages but instead to provide a higher layer of abstraction, on top of classic synchronous languages. It can be considered as a real-time software architecture language that enables to assemble locally mono-periodic synchronous systems into a globally multi-periodic synchronous system.

The preludec compiler generates synchronized multi-task C code, that is independent of the target OS. Communication is achieved by a tailor-made buffering communication protocol. The compilation was defined formally and produces completely deterministic code, which respects the real-time semantics of the original program (period, deadlines, release dates and precedences) as well as its functional semantics (respect of variables consumption). The Prelude compiler produces code for either monocore or multicore architectures.

Documentation

Master course here;
Practical session, the exercises and resources for the FCS example;
Complete definition of the language in my PhD manuscript (see Chapter 4 mainly);
Shorter presentation here or here;
Further references available here;
For installation, check the INSTALL file of the distribution.

Download

You can download Prelude from its forge (the user 'guest' (passwd: 'oneraguest') can be used to file a bug report or access read-only sections of the Forge).

You will need OCaml installed to compile the source distribution, which should be packaged for most Linux distributions, otherwise you can get it from here. To compile the code generated by preludec, the simplest way is to install SchedMCore. You can however use your favorite RTOS instead, following the instructions in the README.

Feedback is welcome and encouraged: Email:julien dot forget at univ-lille1 dot fr

Supported features

The following features are supported by the current distribution:

Language features:
- Synchronous semantics;
- Periodicity constraints (through strictly periodic clocks);
- Deadline constraints;
- Strictly periodic clocks and associated transformations: periodic over-sampling (*^), periodic under-sampling (/^), phase offset (~>), clock tail (tail) and clock concatenation (::);
- Classic synchronous operators: delay (fby), Boolean under-sampling (when) and Boolean over-sampling (merge);
- Clocks polymorphism;
- Types polymorphism (à la ML).
Static analyses:
- Typing;
- Clock calculus;
- Causality analysis;
- Deadline calculus.
Muli-threaded C code generation (independent from the target OS);
Code suited for either monocore or multicore artchitectures.