Properties checked by default by the Fiacre model and the Hippo engine

There are a number of properties which are checked at run time:


UPR or Uninitialized Port Read means that possibly, a codel using a port as in or inout is being called before a call to a codel which use this port as out over all the components in the experiment (this condition has no real meaning ig your model has only one component). This is not a bug per se but clearly, you should investigate the issue to make sure that it is not leading to a problem.

Periodic Task overshoot

Periodic task are associated to timers, which will set the rate at which they should be run. In case a task takes longer than its specified period, it is reported by the Hippo engine, as well as the number of cycle "lost". Again, this may not be a bug, but clearly, if the specified period cannot be satisfied, the design or the specification should be changed.

WCET overshoot

WCET for each codel in the experiment can be provided for various proof on the Fiacre model. At execution time, if a codel takes longer than its WCET, it is reported by the Hippo engine. This can be the result of different causes, but considering that this WCET is also used when verifying the model it may be a good idea to change it.