Project

General

Profile

History

Presentation of the FIACRE/Hippo experiment.

This experiment is based on the FIACRE language; the Hippo engine (aka FIACRE model execution engine) which, providing the addition to the FIACRE language of asynchronous external tasks execution (with start/sync) and event ports (with event port), enables the execution of the model and online V&V; and the TINA toolbox, mostly used for offline V&V of the model.

When installed, the FIACRE template provides three different GenoM3 templates:

  • fiacre/model which produces a FIACRE model of the GenoM component(s). This model is to be used with the TINA tools (selt/sift) 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 inspired from the ros/server 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.

  • 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 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.

Here are links to the resulting models when applied to the specification of the 9 GenoM modules used by Minnie:

Note that the fiacre/model should be different if one considers the PocoLibs vs. ROS Com middleware (i.e. shared memory vs. XML RPC, TCP/IP). In fact, the current model implements the shared memory setup (hence, it checks proper access mutual exclusion).
Note that the fiacre/pocolibs and fiacre/ros models are almost identical. Just the port management part is different. Indeed, pocolibs uses a shared memory model (hence the mutex), while the XML-RPC/TCP-IP model used by ROS does not require such mechanism.

Experiments with the Hippo FIACRE Engine

Regular runs

The two videos show the Hippo FIACRE Engine running on Minnie (PocoLibs version):

Video 1
Video2

This video shows a similar experiment using the ROS version and a more informed display in RVIZ:

Screencast of the ROS version with RVIZ display

Experiment with a FIACRE monitor

This experiment, similar to the one performed with BIP and the BIP Engine, uses Hippo, the FIACRE Engine to monitor some particular conditions online and take action to prevent a problem.

In our example, we modify the automatically synthesized FIACRE model for the whole Minnie experiement to add a FIACRE process (Velodyne_Scans_rmp440_Track_Stopper) which will share a Boolean scan_updated with the process updating the Velodyne PointCloud, and if it detect that the pointcloud has not been updated for 200ms, will stop the robot (i.e. will stop the Track activity of the RMP440 component):

process Velodyne_Scans_rmp440_Track_Stopper(
       &scan_updated:bool,
       &TrackTask_activities: Activities_rmp440_TrackTask_Array, // activities array of the rmp440_TrackTask task
       Track_index: act_inst_rmp440_TrackTask_index_type) is

states monitor_start, monitor_wait, monitor_error

var ignorep:nat

from monitor_start
    ignorep := fiacre_c_print_patch_trace(6); //   {0, "monitor_start entered"} /* 6 */
    on (scan_updated);
    ignorep := fiacre_c_print_patch_trace(7); //   {0, "monitor_start scan_updated"},	/* 7 */
    scan_updated := false;
    to monitor_wait

from monitor_wait
    ignorep := fiacre_c_print_patch_trace(8); //   {0, "monitor_wait entered"} /* 8 */
    select
       wait [200,200];
       ignorep := fiacre_c_print_patch_trace(0); //   {0, "monitor_wait 200 ms elapsed"},	/* 0 */
       to monitor_error
    []
       on (scan_updated);
       ignorep := fiacre_c_print_patch_trace(1); //    {0, "monitor_wait scan_updated."},	/* 1 */
       scan_updated := false;
       to monitor_wait
    end

from monitor_error
   ignorep := fiacre_c_print_patch_trace(4); //    {0, "monitor_error entered"},/* 4 */
   if (TrackTask_activities[Track_index].status = ACT_RUN_FCR) then
       ignorep := fiacre_c_print_patch_trace(2); //   {0, "monitor_error stopping Track"},	/* 2 */
       TrackTask_activities[Track_index].stop := true
   else
       ignorep := fiacre_c_print_patch_trace(9) //   {0, "monitor_error nothing to stop"},	/* 9 */
   end;
   ignorep := fiacre_c_print_patch_trace(5); //  {0, "monitor_error to monitor_start"},/* 5 */
   to monitor_start

The test if (TrackTask_activities[Track_index].status = ACT_RUN_FCR) checks it the robot is currently tracking a speed, and if it is, it stops the activity by setting TrackTask_activities[Track_index].stop to true. This, as a consequence, forces the transition of the Track activity automata in the stopTrack codel which sets linear.x and angular.z speeds at 0 and make the robot stop very abruptly (i.e. without the regular deceleration).

The following video show runs where we inject delay in the velodyne GetScans activity, which result in emergency stops from the robot.

First video shows the Hippo Pocolibs version
Second video shows the Hippo ROS version (with a more detailled RVIZ display)

The corresponding logs of the respective runs can be found here and here.

By searching in the log, the string delay and --PATCH--, one can easily find the places where the delays have been injected and how the monitor responded to each. Note for example that a delay of 100ms is not always sufficient to stop the robot, as the processing time varies and overall, the time between 2 scans may still be within 200ms.