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