Hippo
|
this page exists until a more official HIPPO page is created. |
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 frac compiler for hippo.
Write an Hippo Model
A hippo model is written in Fiacre. The only restriction in the Hippo model 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 (thread) and is scheduled by the operating system. The "regular" Fiacre language does not have a syntax element to describe task activation and termination; therefore, so we have extended 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;
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>
For example:
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:
| Option | Descripton | Mandatory |
|---|---|---|
–help, -h |
show options |
no |
–target, -t=<posix|xenomai> |
define the target |
yes |
–unit, -u = <x><us| ms|s> |
set the time unit (second by default) |
no |
–debug, -d = <inline|scn> |
generate debug information during the execution, scn format can be import in play from Tina toolbox |
no |
–enable, -e = <yes|no> |
print the log trace during the execution |
no |
–lttng, -l = <yes> |
add lltng |
no |
–gdb, -g = <yes> |
add -g option flag to generate debug information to be used by GDB debugger |
no |
–hippolib, -h = <path> |
specify the path (realtive or absolute) of the hippo library |
no |
The compilation is simply done by calling make.
Examples
Some simple examples can be found in the repository `tests. Three more complex examples of robotic applications developped with GenoM3 are given. Two manage a mobile robot (Minnie and Osmosis) while the third one handle a UAV. In these 3 experiments, the Hippo version performs exactly like the regular GenoM pocolibs version.