Overview

Hippo is a toolchain aims to provide tools to design, verify, and generate code for embedded real-time applications to enforce their temporal safety. It is based on the toolbox Tina and the formal language Fiacre.

The main problem addressed by Hippo concerns the generation of an executable that guarantees that the timing constraints are respected. One difficulty is to avoid a semantic gap between the model produced by the designer, the model used by the model-checker, and the executable. For the Hippo toolchain, the code is generated as close as possible to the Time Transition Systems (TTS) model. Therefore, during the generation step, a runtime system is used to produce C code from a Fiacre model that guarantees a control flow that is identical in every detail to the behavior of the TTS.

Install Hippo Toolchain

To use Hippo you need:

• A Linux installation such Ubuntu (if possible patched with preempt-RT and eventually with Xenomai),
• The dedicated version of the compiler frac for hippo.

Write an Hippo Model

A hippo model is written in H-Fiacre, an extension of Fiacre with tasks, events and external functions.

A restriction in Hippo models is to use punctual intervals for the Fiacre temporal statements, i.e., wait [a,a] with a ∈ N. This restriction ensures that the behavior of the system is deterministic.

Moreover, functional treatments are embedded into external functions. These functions are not coded in the model but can be called from Hippo. It is basically a C function with input and output data. Each function is executed in its own task and is scheduled by the operating system. The Fiacre language does not have a syntax element to describe task activation and termination; therefore, so we have extend the language.

Use an External Task

The declaration of a task is done at the beginning of the Hippo model by task t0 (a1 : ty1, ... , an : tyn) : rty is c_foo where c_foo is the name of the C function executed by the task, arg1:ty1, ..., argn:tyn are the parameters and their types used by the function, and rty is the return type.

The task can be called in a Fiacre process using the statement start with the name of the task and the variables for the parameters: start t0 (p1, ..., pn);

The statement sync is used to synchronize a process with the task termination: sync t0 ret; where t0 is the name of the task and ret the variable used to store the return value.

The synchronization of the activation, i.e., start, or the termination i.e., sync, is blocking and immediate, i.e., the transitions that represent start or sync need to be fired as soon as they are enabled. Due to the synchronous implementation of the Hippo runtime, the synchronization of a termination of a task is time-triggered.

Use an External Event

We also add to the Fiacre syntax an external event statement, i.e. a C function that wait an event. An event is declared as event e0 : ty1 # ... # tyn is c_event where c_event is the C waiting bound C function and ty1 # ... # tyn a structued data that carries data from the event.

To synchronize a Fiacre process with the event, we use the usual Fiacre syntax for a synchronisation with a port e ? d1, d2, ..., dn;.

Code External Functions

All functions bound to a task or an event have to be coded in a C file. Data structures of in-out parameters are automatically generated by frac. The function implementation must respect these data structure declarations.

Compile Hippo

First step is to compile the Hippo model with frac. To compile your model (i.e. MyProject.fcr), execute frac MyProject.fcr MyProject.hippo. The result is generated in the repository MyProject.hippo.

Second step consists to compile C files. From the repository of your project call the python scipt to configure the makefile python3 config.py <project-name> <options> (i.e python3 config.py MyProject -t=posix -t=1ms -d=inline -e=yes configures the project MyProject for a posix target with a tick of 1ms and the inline debug during execution is required).

The options are:

The compilation is simply done by calling make.

Examples

Some simple examples can be found in the repository tests. Three more complexe examples of a robotic applications are given. Two concern a mobil robot (Minnie and Osomosis) and one UAV.

Update: July 21, 2020