About Hippo
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 an extension of 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 underlyimg Fiacre. 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.
To use Hippo you need:
A Linux installation such as Ubuntu (if possible patched with preempt-RT and possibly with Xenomai),
The dedicated version of the compiler frac for hippo, available on the Download page.
Projects
A list of projects (past or present) making use of Hippo.
(TBD)