Project

General

Profile

History

Documentation for the GenoM3 Fiacre / Tina / Hippo template

This template can synthesize various Fiacre models for a given GenoM3 specification (one or mode component). The resulting automatically synthesized models can than be used for various V&V activities as provided by the Fiacre / Tina / Hippo tools: model checking, run time verification.

We invite the reader to check the respective pages of the three mentionned tools, but in a nutshell, the high level formal language is Fiacre. Fiacre models can be compiled with frac which can produce a Time Transition Systems (tts) usable with the TINA tool, or the Hippo TTS model executer.

When installed, the FIACRE template provides in fact three different GenoM3 templates, each of them can be invoked on any valid genom3 .gen sepcification.

  • fiacre/model which produces a FIACRE model of the GenoM component(s). This model is to be used with the TINA tools (e.g. selt, sift, nd, etc) for offline model checking. This template has a large number of arguments/options to produce a more or less abstracted model (type genom3 fiacre/model -h to see all the available options). One can also provide a specific client to be used. This is useful for example to validate a particular initialization sequence.

  • fiacre/pocolibs which produces a FIACRE model and the source code to build an Hippo executable using the 'PocoLibs' middleware. The resulting executable can be used in place of the regular PocoLibs module (obtained with the pocolibs/server GenoM3 template). This templace is heavily inspired from the pocolibs/server template.

  • fiacre/ros produces a FIACRE model and the source code to build an Hippo executable for the 'ROS' middleware. The resulting executable can be used in place of the regular ROS module (obtained with the ros/server GenoM3 template). This templace is heavily from the ros/server template. More information on how to use this template…​

The FIACRE models produced for the 3 templates are almost identical. In fact, the 3 models are produced from one original FIACRE template file. The only important differences between the models are:

  • all non deterministic choices (e.g. codels returned values, used for activities automata transition, or control codels success/exception) are handled with FIACRE tasks (start/sync) in the Hippo models, but with select []* end in the offline TINA model (check the Hippo page for more on this).

  • codels execution is really carried on in the Hippo models (with start/sync), but is modeled with a time interval of [0,wcet] (or [wcet,wcet]) in the TINA model.

  • The TINA model must have a client model provided to be consistent and for properties to be checked, otherwise, the model is opened and useless. The Hippo models are "linked" with the client using Hippo event ports and task executions. In this case, the event port handles either the 'PocoLibs Mbox' or the 'ROS CallBackQueue', and the task executions handle the codels calls.

The fact that the online and offline models are almost the same is a very stong argument to show that the model has the proper semantic. Indeed, the online model, being run in place of the regular GenoM module must behave exactly like the real module, otherwise, one can see that the behaviors differ. This is not a formal proof, yet it gives high confidence that the model is "from its observable behavior" point of view, similar in all aspects to the regular 'PocoLibs' or 'ROS' server (module) template. One could argue that it is less 'formal' than writting the formal semantic of a GenoM module and then translating this model in the FIACRE langage, but again, this argument is as good as the absence of errors or too abstacted simplification in the initial formal semantic.