Module Frama_c_kernel.Linear_filter

Compute filters invariants, i.e bounds for each of the filter's state dimensions when the iterations goes to infinity.

A filter corresponds to the following recursive equation :

X[t + 1] = AX[t] + ∑B(ω)ε(ω)[k + 1] + C 

where :

To compute filter invariants, each measure of a given source is supposed bounded by the same interval, represented as a center and a deviation. Each source can thus be bounded by a different interval.

Linear_filter_test is an example using this module.

module Make (Field : Field.S) : sig ... end