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] + \sumB(ω)ε(ω)[k + 1] + C

where :

$n$ is the filter's order ;
$ω$ is a measure's source (for instance, a specific sensor in a cyberphysical system) ;
$m(ω)$ is the delay for the source $ω$ ;
$X[t] \in 𝕂^n$ is the filter's state at iteration t ;
$ε(ω)[t] ∈ 𝕂^{m(ω)}$ is the measure at iteration t for the source $ω$ ;
$A ∈ 𝕂^{nxn}$ is the filter's state matrix ;
$B(ω) ∈ 𝕂^{nxm(ω)}$ is the source matrix for the source $ω$ ;
$C \in 𝕂^n$ is the filter's center.

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